let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p2 <> p1 & p1 <> p3 & p3 <> p2 & angle p2,p1,p3 < PI & angle p1,p3,p2 < PI & angle p3,p2,p1 < PI implies ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI )
assume A1: ( p2 <> p1 & p1 <> p3 & p3 <> p2 & angle p2,p1,p3 < PI & angle p1,p3,p2 < PI & angle p3,p2,p1 < PI ) ; :: thesis: ((angle p2,p1,p3) + (angle p1,p3,p2)) + (angle p3,p2,p1) = PI
then A2: euc2cpx p1 <> euc2cpx p2 by Th6;
A3: euc2cpx p1 <> euc2cpx p3 by A1, Th6;
A4: euc2cpx p3 <> euc2cpx p2 by A1, Th6;
per cases ( 0 = angle (euc2cpx p2),(euc2cpx p1),(euc2cpx p3) or 0 < angle (euc2cpx p2),(euc2cpx p1),(euc2cpx p3) ) by COMPLEX2:84;
suppose A5: 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 A2, A3, A4, A5, 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 A5; :: 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 A5; :: 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 A1, A2, A3, COMPLEX2:98; :: thesis: verum
end;
end;