---

Step * of Lemma geo-congruent-preserves-colinear

∀e:BasicGeometry
  ∀[a,b,c,a',b',c':Point].  (Colinear(a';b';c')) supposing (bc ≅ b'c' and ac ≅ a'c' and ab ≅ a'b' and Colinear(a;b;c))
BY
{ (Auto
   THEN (gColinearCases 8 THENA Auto)
   THEN Try ((D 8 THEN Trivial⋅))
   THEN Try ((gEliminatePoint' (-1) THEN Auto))
   THEN (FLemma `geo-strict-between-implies-between` [-1] THENA Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. Colinear(a;b;c)
9. ab ≅ a'b'
10. ac ≅ a'c'
11. bc ≅ b'c'
12. a-b-c
13. a_b_c
⊢ Colinear(a';b';c')

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. Colinear(a;b;c)
9. ab ≅ a'b'
10. ac ≅ a'c'
11. bc ≅ b'c'
12. b-c-a
13. b_c_a
⊢ Colinear(a';b';c')

3
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. Colinear(a;b;c)
9. ab ≅ a'b'
10. ac ≅ a'c'
11. bc ≅ b'c'
12. c-a-b
13. c_a_b
⊢ Colinear(a';b';c')

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry
    \mforall{}[a,b,c,a',b',c':Point].
        (Colinear(a';b';c'))  supposing  (bc  \00D0  b'c'  and  ac  \00D0  a'c'  and  ab  \00D0  a'b'  and  Colinear(a;b;c))


By

---

Latex:
(Auto
  THEN  (gColinearCases  8  THENA  Auto)
  THEN  Try  ((D  8  THEN  Trivial\mcdot{}))
  THEN  Try  ((gEliminatePoint'  (-1)  THEN  Auto))
  THEN  (FLemma  `geo-strict-between-implies-between`  [-1]  THENA  Auto))

---

Home Index