theorem Th15: :: EUCLID_6:15

for p1, p2, p3, p4, p being Point of (TOP-REAL 2) st p in LSeg (p1,p3) & p in LSeg (p2,p4) & p <> p1 & p <> p2 & p <> p3 & p <> p4 holds
angle (p1,p,p2) = angle (p3,p,p4)