theorem Th15: :: GOBRD11:15

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