let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1,p2,p3 are_mutually_different & angle p1,p2,p3 <= PI implies ( angle p2,p3,p1 <= PI & angle p3,p1,p2 <= PI ) )
assume
p1,p2,p3 are_mutually_different
; :: thesis: ( not angle p1,p2,p3 <= PI or ( angle p2,p3,p1 <= PI & angle p3,p1,p2 <= PI ) )
then
( p1 <> p2 & p1 <> p3 & p2 <> p3 )
by ZFMISC_1:def 5;
then
( euc2cpx p1 <> euc2cpx p2 & euc2cpx p1 <> euc2cpx p3 & euc2cpx p2 <> euc2cpx p3 )
by EUCLID_3:6;
then A1:
( ((angle p1,p2,p3) + (angle p2,p3,p1)) + (angle p3,p1,p2) = PI or ((angle p1,p2,p3) + (angle p2,p3,p1)) + (angle p3,p1,p2) = 5 * PI )
by COMPLEX2:102;
assume A2:
angle p1,p2,p3 <= PI
; :: thesis: ( angle p2,p3,p1 <= PI & angle p3,p1,p2 <= PI )
( angle p2,p3,p1 < 2 * PI & angle p3,p1,p2 < 2 * PI )
by COMPLEX2:84;
then
(angle p2,p3,p1) + (angle p3,p1,p2) < (2 * PI ) + (2 * PI )
by XREAL_1:10;
then A3:
(angle p1,p2,p3) + ((angle p2,p3,p1) + (angle p3,p1,p2)) < PI + (4 * PI )
by A2, XREAL_1:10;
A4:
( angle p1,p2,p3 >= 0 & angle p2,p3,p1 >= 0 & angle p3,p1,p2 >= 0 )
by COMPLEX2:84;
thus
angle p2,p3,p1 <= PI
:: thesis: angle p3,p1,p2 <= PI proof
assume
angle p2,
p3,
p1 > PI
;
:: thesis: contradiction
then
(angle p1,p2,p3) + (angle p2,p3,p1) > 0 + PI
by A4, XREAL_1:10;
hence
contradiction
by A1, A3, A4, XREAL_1:10;
:: thesis: verum
end;
thus
angle p3,p1,p2 <= PI
:: thesis: verumproof
assume
angle p3,
p1,
p2 > PI
;
:: thesis: contradiction
then
(angle p2,p3,p1) + (angle p3,p1,p2) > 0 + PI
by A4, XREAL_1:10;
hence
contradiction
by A1, A3, A4, XREAL_1:10;
:: thesis: verum
end;