---

Step * of Lemma rectangle-sides-cong

No Annotations
∀g:EuclideanPlane. ∀a,b,c,d,e,f:Point.
  (e # ac
  ⇒ f # eb
  ⇒ ac  ⊥b be
  ⇒ df  ⊥e eb
  ⇒ d-e-f
  ⇒ a-b-c
  ⇒ ab ≅ eb
  ⇒ bc ≅ eb
  ⇒ de ≅ eb
  ⇒ ef ≅ eb
  ⇒ {ad ≅ fc ∧ dc ≅ fa})
BY
{ (Auto
   THEN (Assert ae ≅ ce BY
               (InstLemma  `right-angle-SAS` [⌜g⌝;⌜a⌝;⌜b⌝;⌜e⌝;⌜c⌝;⌜b⌝;⌜e⌝]⋅ THEN Auto))
   THEN (Assert db ≅ fb BY
               (InstLemma  `right-angle-SAS` [⌜g⌝;⌜d⌝;⌜e⌝;⌜b⌝;⌜f⌝;⌜e⌝;⌜b⌝]⋅ THEN Auto))) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac  ⊥b be
11. df  ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
⊢ {ad ≅ fc ∧ dc ≅ fa}

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f:Point.
    (e  \#  ac
    {}\mRightarrow{}  f  \#  eb
    {}\mRightarrow{}  ac    \mbot{}b  be
    {}\mRightarrow{}  df    \mbot{}e  eb
    {}\mRightarrow{}  d-e-f
    {}\mRightarrow{}  a-b-c
    {}\mRightarrow{}  ab  \mcong{}  eb
    {}\mRightarrow{}  bc  \mcong{}  eb
    {}\mRightarrow{}  de  \mcong{}  eb
    {}\mRightarrow{}  ef  \mcong{}  eb
    {}\mRightarrow{}  \{ad  \mcong{}  fc  \mwedge{}  dc  \mcong{}  fa\})


By

---

Latex:
(Auto
  THEN  (Assert  ae  \mcong{}  ce  BY
                          (InstLemma    `right-angle-SAS`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  db  \mcong{}  fb  BY
                          (InstLemma    `right-angle-SAS`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)))

---

Home Index