theorem Th13: :: EUCLID11:18

for A, B, C, E being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (E,B,A) = (angle (C,B,A)) / 3 & angle (B,A,E) = (angle (B,A,C)) / 3 holds
A,B,E is_a_triangle