let p1, p4, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( (angle p1,p4,p2) + (angle p2,p4,p3) = angle p1,p4,p3 or (angle p1,p4,p2) + (angle p2,p4,p3) = (angle p1,p4,p3) + (2 * PI ) )
set c1 = euc2cpx (p1 - p4);
set c2 = euc2cpx (p2 - p4);
set c3 = euc2cpx (p3 - p4);
A1: ( (angle (euc2cpx (p1 - p4)),(euc2cpx (p2 - p4))) + (angle (euc2cpx (p2 - p4)),(euc2cpx (p3 - p4))) = angle (euc2cpx (p1 - p4)),(euc2cpx (p3 - p4)) or (angle (euc2cpx (p1 - p4)),(euc2cpx (p2 - p4))) + (angle (euc2cpx (p2 - p4)),(euc2cpx (p3 - p4))) = (angle (euc2cpx (p1 - p4)),(euc2cpx (p3 - p4))) + (2 * PI ) ) by Lm14;
(angle p1,p4,p2) + (angle p2,p4,p3) = (angle (euc2cpx (p1 - p4)),(euc2cpx (p2 - p4))) + (angle p2,p4,p3) by Lm7
.= (angle (euc2cpx (p1 - p4)),(euc2cpx (p2 - p4))) + (angle (euc2cpx (p2 - p4)),(euc2cpx (p3 - p4))) by Lm7 ;
hence ( (angle p1,p4,p2) + (angle p2,p4,p3) = angle p1,p4,p3 or (angle p1,p4,p2) + (angle p2,p4,p3) = (angle p1,p4,p3) + (2 * PI ) ) by A1, Lm7; :: thesis: verum