theorem Th14: :: GOBRD11:14
for P being Subset of (TOP-REAL 2)
for s1 being Real st P = { |[s,r]| where s, r is Real : s <= s1 } holds
P is closed