---

Step * of Lemma eu-lt-null-segment2

∀e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a,b:Point].  (False) supposing ((a = b ∈ Point) and p < |ab|)
BY
{ (Auto THEN HypSubst' (-1) (-2) THEN Auto) }

1
1. e : EuclideanPlane
2. p : {p:Point| O_X_p} 
3. a : Point
4. b : Point
5. p < |bb|
6. a = b ∈ Point
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[p:\{p:Point|  O\_X\_p\}  ].  \mforall{}[a,b:Point].    (False)  supposing  ((a  =  b)  and  p  <  |ab|)


By

---

Latex:
(Auto  THEN  HypSubst'  (-1)  (-2)  THEN  Auto)

---

Home Index