---

Step * 1 of Lemma sq_stable__geo-left-1


1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. ∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
4. a : Point
5. b : Point
6. c : Point
7. ∀a:Point. a ≡ a
8. ∀a,b:Point.  ab ≅ ba
9. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
10. a leftof bc
11. a # bc
12. a leftof cb
⊢ False
BY
{ (((FLemma `use-plane-sep` [-3;-1] THENA Auto) THEN ExRepD) THEN Assert ⌜a ≡ x⌝⋅) }

1
.....assertion..... 
1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. ∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
4. a : Point
5. b : Point
6. c : Point
7. ∀a:Point. a ≡ a
8. ∀a,b:Point.  ab ≅ ba
9. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
10. a leftof bc
11. a # bc
12. a leftof cb
13. x : Point
14. Colinear(b;c;x)
15. B(axa)
⊢ a ≡ x

2
1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. ∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
4. a : Point
5. b : Point
6. c : Point
7. ∀a:Point. a ≡ a
8. ∀a,b:Point.  ab ≅ ba
9. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
10. a leftof bc
11. a # bc
12. a leftof cb
13. x : Point
14. Colinear(b;c;x)
15. B(axa)
16. a ≡ x
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlaneStructure
2.  BasicGeometryAxioms(g)
3.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mneg{}Colinear(a;b;c)))
4.  a  :  Point
5.  b  :  Point
6.  c  :  Point
7.  \mforall{}a:Point.  a  \mequiv{}  a
8.  \mforall{}a,b:Point.    ab  \mcong{}  ba
9.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)
10.  a  leftof  bc
11.  a  \#  bc
12.  a  leftof  cb
\mvdash{}  False


By

---

Latex:
(((FLemma  `use-plane-sep`  [-3;-1]  THENA  Auto)  THEN  ExRepD)  THEN  Assert  \mkleeneopen{}a  \mequiv{}  x\mkleeneclose{}\mcdot{})

---

Home Index