---

Step * of Lemma congruent-half-plane-angles-implies-right-angles

∀g:EuclideanPlane. ∀a,b,c,d:Point.  (c-b-d ⇒ a # cd ⇒ abc ≅a abd ⇒ {Rabd ∧ Rabc})
BY
{ ((Auto THEN (Assert a ≠ b BY (InstLemma `lsep-colinear-sep` [⌜g⌝;⌜a⌝;⌜c⌝;⌜d⌝;⌜b⌝]⋅ THEN Auto)))
   THEN (InstLemma `adjacent-right-angles-supplementary` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto)
   ) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a # cd
8. abc ≅a abd
9. a ≠ b
10. Rabc ⇐⇒ abc ≅a abd
⊢ {Rabd ∧ Rabc}

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (c-b-d  {}\mRightarrow{}  a  \#  cd  {}\mRightarrow{}  abc  \mcong{}\msuba{}  abd  {}\mRightarrow{}  \{Rabd  \mwedge{}  Rabc\})


By

---

Latex:
((Auto  THEN  (Assert  a  \mneq{}  b  BY  (InstLemma  `lsep-colinear-sep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)))
  THEN  (InstLemma  `adjacent-right-angles-supplementary`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index