theorem Th12: :: GOBRD11:12

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