let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C are_mutually_distinct & 0 < angle (A,B,C) & angle (A,B,C) < PI implies ( 0 < angle (B,C,A) & angle (B,C,A) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI ) )
assume that
A1: A,B,C are_mutually_distinct and
A2: ( 0 < angle (A,B,C) & angle (A,B,C) < PI ) ; :: thesis: ( 0 < angle (B,C,A) & angle (B,C,A) < PI & 0 < angle (C,A,B) & 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 & 0 < angle ((euc2cpx A),(euc2cpx B),(euc2cpx C)) & angle ((euc2cpx A),(euc2cpx B),(euc2cpx C)) < PI ) by A1, A2, EUCLID_3:4, EUCLID_3:def 4;
then A3: ( 0 < angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) & 0 < angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) ) by COMPLEX2:84;
then A4: ( 0 < angle (B,C,A) & 0 < angle (C,A,B) ) by EUCLID_3:def 4;
A5: ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI by A1, A2, EUCLID_3:47;

now :: thesis: ( not PI <= angle (B,C,A) & not PI <= angle (C,A,B) )

assume ( PI <= angle (B,C,A) or PI <= angle (C,A,B) ) ; :: thesis: contradiction

per cases then ( PI <= angle (B,C,A) or PI <= angle (C,A,B) ) ;

suppose PI <= angle (B,C,A) ; :: thesis: contradiction

then (angle (A,B,C)) + PI <= (angle (A,B,C)) + (angle (B,C,A)) by XREAL_1:6;
then A6: ((angle (A,B,C)) + PI) + (angle (C,A,B)) <= PI by A5, XREAL_1:6;
0 + PI < (angle (A,B,C)) + PI by A2, XREAL_1:6;
hence contradiction by A4, XREAL_1:8, A6; :: thesis: verum

end;

suppose PI <= angle (C,A,B) ; :: thesis: contradiction

then (angle (A,B,C)) + PI <= (angle (A,B,C)) + (angle (C,A,B)) by XREAL_1:6;
then A7: ((angle (A,B,C)) + PI) + (angle (B,C,A)) <= ((angle (A,B,C)) + (angle (C,A,B))) + (angle (B,C,A)) by XREAL_1:6;
0 + PI < (angle (A,B,C)) + PI by A2, XREAL_1:6;
hence contradiction by A7, A5, A4, XREAL_1:8; :: thesis: verum

end;

end;

end;

hence ( 0 < angle (B,C,A) & angle (B,C,A) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI ) by A3, EUCLID_3:def 4; :: thesis: verum