let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ( angle (A,B,C) = (2 * PI) - (angle (C,B,A)) & angle (B,C,A) = (2 * PI) - (angle (A,C,B)) & angle (C,A,B) = (2 * PI) - (angle (B,A,C)) & angle (B,A,C) = (2 * PI) - (angle (C,A,B)) & angle (A,C,B) = (2 * PI) - (angle (B,C,A)) & angle (C,B,A) = (2 * PI) - (angle (A,B,C)) ) )
assume A,B,C is_a_triangle ; :: thesis: ( angle (A,B,C) = (2 * PI) - (angle (C,B,A)) & angle (B,C,A) = (2 * PI) - (angle (A,C,B)) & angle (C,A,B) = (2 * PI) - (angle (B,A,C)) & angle (B,A,C) = (2 * PI) - (angle (C,A,B)) & angle (A,C,B) = (2 * PI) - (angle (B,C,A)) & angle (C,B,A) = (2 * PI) - (angle (A,B,C)) )
then ( B,C,A is_a_triangle & C,A,B is_a_triangle & B,A,C is_a_triangle & A,C,B is_a_triangle & C,B,A is_a_triangle ) by MENELAUS:15;
hence ( angle (A,B,C) = (2 * PI) - (angle (C,B,A)) & angle (B,C,A) = (2 * PI) - (angle (A,C,B)) & angle (C,A,B) = (2 * PI) - (angle (B,A,C)) & angle (B,A,C) = (2 * PI) - (angle (C,A,B)) & angle (A,C,B) = (2 * PI) - (angle (B,C,A)) & angle (C,B,A) = (2 * PI) - (angle (A,B,C)) ) by Lm9; :: thesis: verum