theorem Th9: :: TOPREAL3:9

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