let P be Subset of (TOP-REAL 2); :: thesis: for s1 being Real st P = { |[s,r]| where s, r is Real : s1 <= s } holds
P is closed
let s1 be Real; :: thesis: ( P = { |[s,r]| where s, r is Real : s1 <= s } implies P is closed )
assume A1: P = { |[s,r]| where s, r is Real : s >= s1 } ; :: thesis: P is closed
reconsider P1 = { |[s,r]| where s, r is Real : s < s1 } as Subset of (TOP-REAL 2) by Lm8;
A2: P = P1 ` by A1, Th10;
P1 is open by JORDAN1:26;
hence P is closed by A2, TOPS_1:30; :: thesis: verum