let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C are_mutually_distinct & angle (A,B,C) > PI implies ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = 5 * PI )
assume that
A1: A,B,C are_mutually_distinct and
A2: angle (A,B,C) > PI ; :: thesis: ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = 5 * PI
( angle (A,B,C) <> 0 & angle (B,C,A) <> 0 & angle (C,A,B) <> 0 ) by A1, A2, COMPTRIG:5, EUCLID_6:24;
then A3: ( 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)) ) by EUCLID_3:38;
(2 * PI) - (angle (A,B,C)) < (2 * PI) - PI by A2, XREAL_1:15;
then ((angle (C,B,A)) + (angle (B,A,C))) + (angle (A,C,B)) = PI by A1, A3, EUCLID_3:47;
hence ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = 5 * PI by A3; :: thesis: verum