let p1, p2, p3 be Point of (TOP-REAL 2); ( p2 <> p1 & p1 <> p3 & p3 <> p2 & angle (p2,p1,p3) < PI implies ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI )
assume that
A1:
( p2 <> p1 & p1 <> p3 )
and
A2:
p3 <> p2
and
A3:
angle (p2,p1,p3) < PI
; ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
A4:
( euc2cpx p1 <> euc2cpx p2 & euc2cpx p1 <> euc2cpx p3 )
by A1, Th4;
A5:
euc2cpx p3 <> euc2cpx p2
by A2, Th4;
per cases
( 0 = angle ((euc2cpx p2),(euc2cpx p1),(euc2cpx p3)) or 0 < angle ((euc2cpx p2),(euc2cpx p1),(euc2cpx p3)) )
by COMPLEX2:70;
suppose A6:
0 = angle (
(euc2cpx p2),
(euc2cpx p1),
(euc2cpx p3))
;
((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI now ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI per cases
( ( angle ((euc2cpx p1),(euc2cpx p3),(euc2cpx p2)) = 0 & angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) = PI ) or ( angle ((euc2cpx p1),(euc2cpx p3),(euc2cpx p2)) = PI & angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) = 0 ) )
by A4, A5, A6, COMPLEX2:87;
suppose
(
angle (
(euc2cpx p1),
(euc2cpx p3),
(euc2cpx p2))
= 0 &
angle (
(euc2cpx p3),
(euc2cpx p2),
(euc2cpx p1))
= PI )
;
((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI end; suppose
(
angle (
(euc2cpx p1),
(euc2cpx p3),
(euc2cpx p2))
= PI &
angle (
(euc2cpx p3),
(euc2cpx p2),
(euc2cpx p1))
= 0 )
;
((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI end; end; end; hence
((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
;
verum end; end;