theorem Th6: :: GOBOARD7:6

for p, q, p1 being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & p `2 = q `2 holds
p1 `2 = q `2