theorem Th29: :: JORDAN12:29

for p1, p2, p3, p4, p being Point of (TOP-REAL 2) st ( ( p1 `1 = p2 `1 & p3 `1 = p4 `1 ) or ( p1 `2 = p2 `2 & p3 `2 = p4 `2 ) ) & (LSeg (p1,p2)) /\ (LSeg (p3,p4)) = {p} & not p = p1 & not p = p2 holds
p = p3