Step
*
1
of Lemma
geo-SCS_wf
1. g : EuclideanPlane
2. c : Point
3. d : Point
4. a : Point
5. b : Point
6. b ≠ a ∧ c_b_d
7. v : Point
8. cv ≅ cd ∧ a_b_v ∧ (b ≠ d
⇒ b ≠ v)
9. a' : Point
10. a_v_a'
11. av ≅ va'
12. b_v_a'
⊢ SC(a';b;c;d) ∈ {v@0:Point| cv@0 ≅ cd ∧ (v@0_b_v ∧ Colinear(a;b;v@0)) ∧ (b ≠ d
⇒ v@0 ≠ v)}
BY
{ (DoSubsume THEN Auto THEN (Thin (-1) THEN (D 0 THENA Auto)) THEN D -1 THEN MemTypeCD THEN Auto) }
Latex:
Latex:
1. g : EuclideanPlane
2. c : Point
3. d : Point
4. a : Point
5. b : Point
6. b \mneq{} a \mwedge{} c\_b\_d
7. v : Point
8. cv \mcong{} cd \mwedge{} a\_b\_v \mwedge{} (b \mneq{} d {}\mRightarrow{} b \mneq{} v)
9. a' : Point
10. a\_v\_a'
11. av \mcong{} va'
12. b\_v\_a'
\mvdash{} SC(a';b;c;d) \mmember{} \{v@0:Point| cv@0 \mcong{} cd \mwedge{} (v@0\_b\_v \mwedge{} Colinear(a;b;v@0)) \mwedge{} (b \mneq{} d {}\mRightarrow{} v@0 \mneq{} v)\}
By
Latex:
(DoSubsume THEN Auto THEN (Thin (-1) THEN (D 0 THENA Auto)) THEN D -1 THEN MemTypeCD THEN Auto)
Home
Index