theorem Th5: :: GOBOARD7:5

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