---

Step * of Lemma eu-5segSAS

∀e:EuclideanPlane. ∀a,b,c,f,g,A,B,C,F,G:Point.
  (af=AF ∧ fb=FB ∧ bc=BC ∧ ag=AG ∧ gc=GC) ⇒ fg=FG 
  supposing (Triangle(a;f;g) ∧ Triangle(A;F;G)) ∧ a_f_b ∧ a_g_c ∧ A_F_B ∧ A_G_C
BY
{ (Auto THEN Unhide THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. f : Point
6. g : Point
7. A : Point
8. B : Point
9. C : Point
10. F : Point
11. G : Point
12. Triangle(a;f;g)
13. Triangle(A;F;G)
14. a_f_b
15. a_g_c
16. A_F_B
17. A_G_C
18. af=AF
19. fb=FB
20. bc=BC
21. ag=AG
22. gc=GC
⊢ fg=FG

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,f,g,A,B,C,F,G:Point.
    (af=AF  \mwedge{}  fb=FB  \mwedge{}  bc=BC  \mwedge{}  ag=AG  \mwedge{}  gc=GC)  {}\mRightarrow{}  fg=FG 
    supposing  (Triangle(a;f;g)  \mwedge{}  Triangle(A;F;G))  \mwedge{}  a\_f\_b  \mwedge{}  a\_g\_c  \mwedge{}  A\_F\_B  \mwedge{}  A\_G\_C


By

---

Latex:
(Auto  THEN  Unhide  THEN  Auto)

---

Home Index