---

Step * 1 of Lemma not-geo-lt-points


1. g : EuclideanPlane
2. p : {p:Point| B(OXp)} 
3. q : {p:Point| B(OXp)} 
4. ¬(p ≤ q ∧ p # q)
⊢ q ≤ p
BY
{ ((RWO "geo-le-iff-between-points" (-1) THENA Auto)
   THEN (RWO "geo-le-iff-between-points" 0 THENA Auto)
   THEN DSetVars
   THEN Unhide
   THEN Auto) }

1
1. g : EuclideanPlane
2. p : Point
3. B(OXp)
4. q : Point
5. B(OXq)
6. ¬(B(Xpq) ∧ p # q)
⊢ B(Xqp)

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  p  :  \{p:Point|  B(OXp)\} 
3.  q  :  \{p:Point|  B(OXp)\} 
4.  \mneg{}(p  \mleq{}  q  \mwedge{}  p  \#  q)
\mvdash{}  q  \mleq{}  p


By

---

Latex:
((RWO  "geo-le-iff-between-points"  (-1)  THENA  Auto)
  THEN  (RWO  "geo-le-iff-between-points"  0  THENA  Auto)
  THEN  DSetVars
  THEN  Unhide
  THEN  Auto)

---

Home Index