let p1, p2, p3, p4 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