Step
*
of Lemma
geo-colinear-transitivity
∀e:EuclideanPlane
∀[A,C,B,D:Point]. (Colinear(A;B;C)
⇒ Colinear(B;C;D)
⇒ B ≠ C
⇒ {Colinear(A;C;D) ∧ Colinear(A;B;D)})
BY
{ (Auto
THEN Unfold `guard` 0
THEN All (RWO "not-lsep-iff-colinear<")⋅
THEN Auto
THEN (D 0 THENA Auto)
THEN FLemma `lsep-implies-sep` [-1]
THEN Auto) }
1
1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. ¬A # BC
7. ¬B # CD
8. B ≠ C
9. A # CD
10. A ≠ C
11. A ≠ D
12. C ≠ D
⊢ False
2
1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. ¬A # BC
7. ¬B # CD
8. B ≠ C
9. ¬A # CD
10. A # BD
11. A ≠ B
12. A ≠ D
13. B ≠ D
⊢ False
Latex:
Latex:
\mforall{}e:EuclideanPlane
\mforall{}[A,C,B,D:Point].
(Colinear(A;B;C) {}\mRightarrow{} Colinear(B;C;D) {}\mRightarrow{} B \mneq{} C {}\mRightarrow{} \{Colinear(A;C;D) \mwedge{} Colinear(A;B;D)\})
By
Latex:
(Auto
THEN Unfold `guard` 0
THEN All (RWO "not-lsep-iff-colinear<")\mcdot{}
THEN Auto
THEN (D 0 THENA Auto)
THEN FLemma `lsep-implies-sep` [-1]
THEN Auto)
Home
Index