theorem :: TOPREAL3:12

for p being Point of (TOP-REAL 2)
for r, r1, s1 being Real st p in LSeg (|[r1,r]|,|[s1,r]|) holds
p `2 = r