let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C are_mutually_distinct & angle (A,B,C) > PI implies ( angle (B,C,A) > PI & angle (C,A,B) > PI ) )
assume A1: ( A,B,C are_mutually_distinct & angle (A,B,C) > PI ) ; :: thesis: ( angle (B,C,A) > PI & angle (C,A,B) > PI )
set z1 = euc2cpx A;
set z2 = euc2cpx B;
set z3 = euc2cpx C;
( euc2cpx A <> euc2cpx B & euc2cpx B <> euc2cpx C & euc2cpx A <> euc2cpx C & angle ((euc2cpx A),(euc2cpx B),(euc2cpx C)) > PI ) by A1, EUCLID_3:4, EUCLID_3:def 4;
then ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) > PI & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) > PI ) by COMPLEX2:85;
hence ( angle (B,C,A) > PI & angle (C,A,B) > PI ) by EUCLID_3:def 4; :: thesis: verum