---

Step * 2 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
     ∀[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)
⊢ ∀e:EuclideanPlane
    ∀[a,b,A,B,c,d,C,D:Point].
      (ad ≅ AD ∧ bd ≅ BD ∧ cd ≅ CD) supposing (ab  ⊥d dc and AB  ⊥D DC and bc ≅ BC and ac ≅ AC and ab ≅ AB)
BY
{ (Thin 1
   THEN RepeatFor 9 (ParallelLast')
   THEN (UnivCD THENA Auto)
   THEN (StableCases ⌜a ≠ b⌝⋅ THENA (Auto THEN RepeatFor 2 ((BLemma `stable__and` THEN Auto))))
   THEN Try ((Fold `geo-eq` (-1) THEN FLemma `geo-perp-in-not-eq` [-2] THEN Auto))
   THEN ThinTrivial
   THEN 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. ab ≅ AB
11. ac ≅ AC
12. bc ≅ BC
13. AB  ⊥D DC
14. ab  ⊥d dc
15. a ≠ b
16. ad ≅ AD
17. bd ≅ BD
18. ad ≅ AD
19. bd ≅ BD
⊢ cd ≅ CD

---

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.  \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)
\mvdash{}  \mforall{}e:EuclideanPlane
        \mforall{}[a,b,A,B,c,d,C,D:Point].
            (ad  \mcong{}  AD  \mwedge{}  bd  \mcong{}  BD  \mwedge{}  cd  \mcong{}  CD)  supposing 
                  (ab    \mbot{}d  dc  and 
                  AB    \mbot{}D  DC  and 
                  bc  \mcong{}  BC  and 
                  ac  \mcong{}  AC  and 
                  ab  \mcong{}  AB)


By

---

Latex:
(Thin  1
  THEN  RepeatFor  9  (ParallelLast')
  THEN  (UnivCD  THENA  Auto)
  THEN  (StableCases  \mkleeneopen{}a  \mneq{}  b\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  RepeatFor  2  ((BLemma  `stable\_\_and`  THEN  Auto))))
  THEN  Try  ((Fold  `geo-eq`  (-1)  THEN  FLemma  `geo-perp-in-not-eq`  [-2]  THEN  Auto))
  THEN  ThinTrivial
  THEN  Auto)

---

Home Index