---

Step * of Lemma r2-basic-geo-axioms

No Annotations
BasicGeometryAxioms(r2-eu-prim())
BY
{ (RepUR ``basic-geo-axioms r2-eu-prim mk-eu-prim`` 0 THEN SplitAndConcl) }

1
∀a,b,c,d:Point.  (ab>cd ⇒ ab ≥ cd)

2
∀a,b,c:Point.  (ba>ac ⇒ b # c)

3
∀a,b,c:Point.  bc ≥ aa

4
∀a,b,c,d,e,f:Point.  (ab>cd ⇒ cd ≥ ef ⇒ ab>ef)

5
∀a,b,c,d,e,f:Point.  (ab ≥ cd ⇒ cd>ef ⇒ ab>ef)

6
∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)

7
∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)

8
∀a,b,c:Point.  (a leftof bc ⇒ b # c)

9
∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))

10
∀a,b,c,d,A,B,C,D:Point.  (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)

11
∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))

12
∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)

13
∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)

---

Latex:

---

Latex:
No  Annotations
BasicGeometryAxioms(r2-eu-prim())


By

---

Latex:
(RepUR  ``basic-geo-axioms  r2-eu-prim  mk-eu-prim``  0  THEN  SplitAndConcl)

---

Home Index