---

Step * 1 of Lemma perp-in-congruence

.....assertion..... 
∀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)
BY
{ (Intros THEN (Unhide THENA Auto)) }

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. c # ab
11. C # AB
12. ab ≅ AB
13. ac ≅ AC
14. bc ≅ BC
15. AB  ⊥D DC
16. ab  ⊥d dc
⊢ ad ≅ AD ∧ bd ≅ BD

---

Latex:

---

Latex:
.....assertion..... 
\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)


By

---

Latex:
(Intros  THEN  (Unhide  THENA  Auto))

---

Home Index