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 (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 (C,B,A) = (2 * PI) - (angle (A,B,C)) )
then angle (A,B,C) <> 0 by Thm19;
hence angle (A,B,C) = (2 * PI) - (angle (C,B,A)) by EUCLID_3:38; :: thesis: angle (C,B,A) = (2 * PI) - (angle (A,B,C))
hence angle (C,B,A) = (2 * PI) - (angle (A,B,C)) ; :: thesis: verum