theorem Th10: :: TOPREAL3:10

for r, r1, s1 being Real st r1 <= s1 holds
{ p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } = LSeg (|[r1,r]|,|[s1,r]|)