---

Step * 2 1 2 of Lemma perp-in-congruence


1. ∀e:EuclideanPlane
     ∀[a,b,A,B,c,d,C,D:Point].
       (ad ≅ AD ∧ bd ≅ BD) supposing (ab  ⊥d dc and AB  ⊥D DC and bc ≅ BC and ac ≅ AC and ab ≅ AB and C # AB and c # ab)
2. e : EuclideanPlane
3. a : Point
4. b : Point
5. A : Point
6. B : Point
7. c : Point
8. d : Point
9. C : Point
10. D : Point
11. a ≠ b
12. ab ≅ AB
13. ac ≅ AC
14. bc ≅ BC
15. AB  ⊥D DC
16. ab  ⊥d dc
17. ¬c # ab
⊢ ad ≅ AD ∧ bd ≅ BD
BY
{ (Thin 1
   THEN (Assert Colinear(c;a;b) BY
               (RWO "not-lsep-iff-colinear" (-1) THEN Auto))
   THEN Thin (-2)
   THEN (Assert Colinear(C;A;B) BY
               EasyGeometry)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. A : Point
5. B : Point
6. c : Point
7. d : Point
8. C : Point
9. D : Point
10. a ≠ b
11. ab ≅ AB
12. ac ≅ AC
13. bc ≅ BC
14. AB  ⊥D DC
15. ab  ⊥d dc
16. Colinear(c;a;b)
17. Colinear(C;A;B)
⊢ ad ≅ AD ∧ bd ≅ BD

---

Latex:

---

Latex:

1.  \mforall{}e:EuclideanPlane
          \mforall{}[a,b,A,B,c,d,C,D:Point].
              (ad  \mcong{}  AD  \mwedge{}  bd  \mcong{}  BD)  supposing 
                    (ab    \mbot{}d  dc  and 
                    AB    \mbot{}D  DC  and 
                    bc  \mcong{}  BC  and 
                    ac  \mcong{}  AC  and 
                    ab  \mcong{}  AB  and 
                    C  \#  AB  and 
                    c  \#  ab)
2.  e  :  EuclideanPlane
3.  a  :  Point
4.  b  :  Point
5.  A  :  Point
6.  B  :  Point
7.  c  :  Point
8.  d  :  Point
9.  C  :  Point
10.  D  :  Point
11.  a  \mneq{}  b
12.  ab  \mcong{}  AB
13.  ac  \mcong{}  AC
14.  bc  \mcong{}  BC
15.  AB    \mbot{}D  DC
16.  ab    \mbot{}d  dc
17.  \mneg{}c  \#  ab
\mvdash{}  ad  \mcong{}  AD  \mwedge{}  bd  \mcong{}  BD


By

---

Latex:
(Thin  1
  THEN  (Assert  Colinear(c;a;b)  BY
                          (RWO  "not-lsep-iff-colinear"  (-1)  THEN  Auto))
  THEN  Thin  (-2)
  THEN  (Assert  Colinear(C;A;B)  BY
                          EasyGeometry))

---

Home Index