---

Step * 2 1 of Lemma perp-in-congruence

.....assertion..... 
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)
⊢ ∀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 a ≠ b)
BY
{ ((Intros THEN (Unhide THENA Auto)) THEN (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
⊢ 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
⊢ ad ≅ AD ∧ bd ≅ BD

---

Latex:

---

Latex:
.....assertion..... 
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)
\mvdash{}  \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 
                  a  \mneq{}  b)


By

---

Latex:
((Intros  THEN  (Unhide  THENA  Auto))
  THEN  (StableCases  \mkleeneopen{}c  \#  ab\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  BLemma  `stable\_\_and`  THEN  Auto))
  )

---

Home Index