---

Step * of Lemma geo-5segSAS

No Annotations
∀e:BasicGeometry. ∀a,b,c,f,g,A,B,C,F,G:Point.
  (af ≅ AF ∧ fb ≅ FB ∧ bc ≅ BC ∧ ag ≅ AG ∧ gc ≅ GC) ⇒ fg ≅ FG supposing B(afb) ∧ B(agc) ∧ B(AFB) ∧ B(AGC)
BY
{ (Auto THEN EasyGeometry') }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,f,g,A,B,C,F,G:Point.
    (af  \mcong{}  AF  \mwedge{}  fb  \mcong{}  FB  \mwedge{}  bc  \mcong{}  BC  \mwedge{}  ag  \mcong{}  AG  \mwedge{}  gc  \mcong{}  GC)  {}\mRightarrow{}  fg  \mcong{}  FG 
    supposing  B(afb)  \mwedge{}  B(agc)  \mwedge{}  B(AFB)  \mwedge{}  B(AGC)


By

---

Latex:
(Auto  THEN  EasyGeometry')

---

Home Index