Nuprl 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


Proof

Error : references
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


Date html generated: 2017_02_21-AM-10_18_47
Last ObjectModification: 2016_06_01-PM-01_05_15

Theory : euclidean!geometry


Home Index