---

Step * of Lemma opp-side-congruence-lemma

No Annotations
∀e:EuclideanPlane
  ∀[a,b,A,B,c,d,C,D:Point].
    (cd ≅ CD) supposing 
       (C leftof AB and 
       D leftof BA and 
       c leftof ab and 
       d leftof ba and 
       a # b and 
       bd ≅ BD and 
       ad ≅ AD and 
       bc ≅ BC and 
       ac ≅ AC and 
       ab ≅ AB)
BY
{ (Auto
   THEN (Assert a # b ∧ c # a ∧ a # d BY
               Auto)
   THEN (Assert cab ≅a CAB ∧ bad ≅a BAD ∧ cad ≅a CAD 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. ab ≅ AB
11. ac ≅ AC
12. bc ≅ BC
13. ad ≅ AD
14. bd ≅ BD
15. a # b
16. d leftof ba
17. c leftof ab
18. D leftof BA
19. C leftof AB
20. a # b ∧ c # a ∧ a # d
21. cab ≅a CAB ∧ bad ≅a BAD ∧ cad ≅a CAD
⊢ cd ≅ CD

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,A,B,c,d,C,D:Point].
        (cd  \mcong{}  CD)  supposing 
              (C  leftof  AB  and 
              D  leftof  BA  and 
              c  leftof  ab  and 
              d  leftof  ba  and 
              a  \#  b  and 
              bd  \mcong{}  BD  and 
              ad  \mcong{}  AD  and 
              bc  \mcong{}  BC  and 
              ac  \mcong{}  AC  and 
              ab  \mcong{}  AB)


By

---

Latex:
(Auto
  THEN  (Assert  a  \#  b  \mwedge{}  c  \#  a  \mwedge{}  a  \#  d  BY
                          Auto)
  THEN  (Assert  cab  \mcong{}\msuba{}  CAB  \mwedge{}  bad  \mcong{}\msuba{}  BAD  \mwedge{}  cad  \mcong{}\msuba{}  CAD  BY
                          EasyGeometry))

---

Home Index