---

Step * of Lemma cong-angle-out-exists1

∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.  (abc ≅a xyz ⇒ (∃x',z':Point. (out(y x'x) ∧ out(y z'z) ∧ Cong3(x'yz',abc))))
BY
{ (Auto THEN (Assert (x ≠ y ∧ y ≠ z) ∧ a ≠ b ∧ c ≠ b BY (D -1 THEN Auto))) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc ≅a xyz
9. (x ≠ y ∧ y ≠ z) ∧ a ≠ b ∧ c ≠ b
⊢ ∃x',z':Point. (out(y x'x) ∧ out(y z'z) ∧ Cong3(x'yz',abc))

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (abc  \mcong{}\msuba{}  xyz  {}\mRightarrow{}  (\mexists{}x',z':Point.  (out(y  x'x)  \mwedge{}  out(y  z'z)  \mwedge{}  Cong3(x'yz',abc))))


By

---

Latex:
(Auto  THEN  (Assert  (x  \mneq{}  y  \mwedge{}  y  \mneq{}  z)  \mwedge{}  a  \mneq{}  b  \mwedge{}  c  \mneq{}  b  BY  (D  -1  THEN  Auto)))

---

Home Index