let a, b, c, e, f, g be POINT of TarskiEuclid2Space; :: thesis: ( Tn2TR a, Tn2TR b, Tn2TR c is_a_triangle & angle ((Tn2TR a),(Tn2TR b),(Tn2TR c)) < PI & angle ((Tn2TR e),(Tn2TR c),(Tn2TR a)) = (angle ((Tn2TR b),(Tn2TR c),(Tn2TR a))) / 3 & angle ((Tn2TR c),(Tn2TR a),(Tn2TR e)) = (angle ((Tn2TR c),(Tn2TR a),(Tn2TR b))) / 3 & angle ((Tn2TR a),(Tn2TR b),(Tn2TR f)) = (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) / 3 & angle ((Tn2TR f),(Tn2TR a),(Tn2TR b)) = (angle ((Tn2TR c),(Tn2TR a),(Tn2TR b))) / 3 & angle ((Tn2TR b),(Tn2TR c),(Tn2TR g)) = (angle ((Tn2TR b),(Tn2TR c),(Tn2TR a))) / 3 & angle ((Tn2TR g),(Tn2TR b),(Tn2TR c)) = (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) / 3 implies ( dist (f,e) = dist (g,f) & dist (f,e) = dist (e,g) & dist (g,f) = dist (e,g) ) )
assume A1: ( Tn2TR a, Tn2TR b, Tn2TR c is_a_triangle & angle ((Tn2TR a),(Tn2TR b),(Tn2TR c)) < PI & angle ((Tn2TR e),(Tn2TR c),(Tn2TR a)) = (angle ((Tn2TR b),(Tn2TR c),(Tn2TR a))) / 3 & angle ((Tn2TR c),(Tn2TR a),(Tn2TR e)) = (angle ((Tn2TR c),(Tn2TR a),(Tn2TR b))) / 3 & angle ((Tn2TR a),(Tn2TR b),(Tn2TR f)) = (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) / 3 & angle ((Tn2TR f),(Tn2TR a),(Tn2TR b)) = (angle ((Tn2TR c),(Tn2TR a),(Tn2TR b))) / 3 & angle ((Tn2TR b),(Tn2TR c),(Tn2TR g)) = (angle ((Tn2TR b),(Tn2TR c),(Tn2TR a))) / 3 & angle ((Tn2TR g),(Tn2TR b),(Tn2TR c)) = (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) / 3 ) ; :: thesis: ( dist (f,e) = dist (g,f) & dist (f,e) = dist (e,g) & dist (g,f) = dist (e,g) )
( |.((Tn2TR f) - (Tn2TR e)).| = dist (f,e) & |.((Tn2TR g) - (Tn2TR f)).| = dist (g,f) & |.((Tn2TR e) - (Tn2TR g)).| = dist (e,g) ) by ThEquiv;
hence ( dist (f,e) = dist (g,f) & dist (f,e) = dist (e,g) & dist (g,f) = dist (e,g) ) by A1, EUCLID11:23; :: thesis: verum