theorem Th32: :: TOPREAL3:32

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