theorem Th13: :: GOBRD11:13

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