---

Step * 2 of Lemma rng-pps_wf

.....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))
BY
{ Auto }

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index