---

Step * of Lemma rng-pps_wf

∀r:IntegDom{i}. ∀[eq:EqDecider(|r|)]. (rng-pps(r;eq) ∈ ProjectivePlane)
BY
{ (Auto THEN (MemTypeCD THENW Auto)) }

1
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ rng-pps(r;eq) ∈ ProjectivePlaneStructureComplete

2
.....set predicate..... 
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ BasicProjectiveGeometryAxioms(rng-pps(r;eq)) ∧ triangle-axiom1(rng-pps(r;eq)) ∧ triangle-axiom2(rng-pps(r;eq))

---

Latex:

---

Latex:
\mforall{}r:IntegDom\{i\}.  \mforall{}[eq:EqDecider(|r|)].  (rng-pps(r;eq)  \mmember{}  ProjectivePlane)


By

---

Latex:
(Auto  THEN  (MemTypeCD  THENW  Auto))

---

Home Index