theorem :: GTARSKI2:14

for a, b, c, e, f, g being POINT of TarskiEuclid2Space st 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 holds
( dist (f,e) = dist (g,f) & dist (f,e) = dist (e,g) & dist (g,f) = dist (e,g) )