theorem Th29: :: TOPREAL3:29

for p, q being Point of (TOP-REAL 2) holds (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) = {|[(p `1),(q `2)]|}