theorem Th31: :: TOPREAL3:31

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