---

Step * of Lemma geo-lt-add1

∀e:BasicGeometry. ∀p,q:{a:Point| O_X_a} . ∀r:{a:Point| O_X_a ∧ (|Xa| = p + q ∈ Length)} .  (X ≠ p ⇒ X ≠ q ⇒ p < r)
BY
{ (Auto
   THEN (gProperProlong ⌜X⌝⌜p⌝`b'⌜X⌝⌜q⌝⋅ THEN Auto)
   THEN (InstLemma `geo-construction-unicity-from-first` [⌜e⌝;⌜O⌝;⌜X⌝;⌜b⌝;⌜r⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. e : BasicGeometry
2. p : {a:Point| O_X_a} 
3. q : {a:Point| O_X_a} 
4. r : {a:Point| O_X_a ∧ (|Xa| = p + q ∈ Length)} 
5. X ≠ p
6. X ≠ q
7. b : Point
8. X-p-b
9. pb ≅ Xq
⊢ O_X_b

2
.....antecedent..... 
1. e : BasicGeometry
2. p : {a:Point| O_X_a} 
3. q : {a:Point| O_X_a} 
4. r : {a:Point| O_X_a ∧ (|Xa| = p + q ∈ Length)} 
5. X ≠ p
6. X ≠ q
7. b : Point
8. X-p-b
9. pb ≅ Xq
⊢ Or ≅ Ob

3
1. e : BasicGeometry
2. p : {a:Point| O_X_a} 
3. q : {a:Point| O_X_a} 
4. r : {a:Point| O_X_a ∧ (|Xa| = p + q ∈ Length)} 
5. X ≠ p
6. X ≠ q
7. b : Point
8. X-p-b
9. pb ≅ Xq
10. b ≡ r
⊢ p < r

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,q:\{a:Point|  O\_X\_a\}  .  \mforall{}r:\{a:Point|  O\_X\_a  \mwedge{}  (|Xa|  =  p  +  q)\}  .
    (X  \mneq{}  p  {}\mRightarrow{}  X  \mneq{}  q  {}\mRightarrow{}  p  <  r)


By

---

Latex:
(Auto
  THEN  (gProperProlong  \mkleeneopen{}X\mkleeneclose{}\mkleeneopen{}p\mkleeneclose{}`b'\mkleeneopen{}X\mkleeneclose{}\mkleeneopen{}q\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `geo-construction-unicity-from-first`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index