---

Step * 2 1 1 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
{ (StableCases ⌜C # AB⌝⋅ THENA (Auto THEN BLemma `stable__and` THEN Auto)) }

1
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
18. C # AB
⊢ ad ≅ AD ∧ bd ≅ BD

2
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
18. ¬C # AB
⊢ 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.  c  \#  ab
\mvdash{}  ad  \mcong{}  AD  \mwedge{}  bd  \mcong{}  BD


By

---

Latex:
(StableCases  \mkleeneopen{}C  \#  AB\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  BLemma  `stable\_\_and`  THEN  Auto))

---

Home Index