let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI
A4: ( euc2cpx p1 <> euc2cpx p2 & euc2cpx p1 <> euc2cpx p3 ) by A1, Th6;
A5: euc2cpx p3 <> euc2cpx p2 by A2, Th6;

per cases ( 0 = angle (euc2cpx p2),(euc2cpx p1),(euc2cpx p3) or 0 < angle (euc2cpx p2),(euc2cpx p1),(euc2cpx p3) ) by COMPLEX2:84;

suppose A6: 0 = angle (euc2cpx p2),(euc2cpx p1),(euc2cpx p3) ; :: thesis: ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI

now

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:101;

suppose ( angle (euc2cpx p1),(euc2cpx p3),(euc2cpx p2) = 0 & angle (euc2cpx p3),(euc2cpx p2),(euc2cpx p1) = PI ) ; :: thesis: ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI

hence ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI by A6; :: thesis: verum

end;

suppose ( angle (euc2cpx p1),(euc2cpx p3),(euc2cpx p2) = PI & angle (euc2cpx p3),(euc2cpx p2),(euc2cpx p1) = 0 ) ; :: thesis: ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI

hence ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI by A6; :: thesis: verum

end;

end;

end;

hence ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI ; :: thesis: verum

end;

suppose 0 < angle (euc2cpx p2),(euc2cpx p1),(euc2cpx p3) ; :: thesis: ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI

hence ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI by A3, A4, COMPLEX2:98; :: thesis: verum

end;

end;