theorem Th30: :: TOPREAL3:30

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