theorem :: EUCLID_6:46

for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle (p1,p2,p3) = (2 * (angle (p4,p5,p6))) - (4 * PI) by Lm5;