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

P is closed

let s1 be Real; :: thesis: ( P = { |[r,s]| where r, s is Real : s1 <= s } implies P is closed )

reconsider P1 = { |[r,s]| where r, s is Real : s1 > s } as Subset of (TOP-REAL 2) by Lm6;

assume P = { |[r,s]| where r, s is Real : s1 <= s } ; :: thesis: P is closed

then A1: P = P1 ` by Th9;

P1 is open by JORDAN1:23;

hence P is closed by A1, TOPS_1:4; :: thesis: verum

P is closed

let s1 be Real; :: thesis: ( P = { |[r,s]| where r, s is Real : s1 <= s } implies P is closed )

reconsider P1 = { |[r,s]| where r, s is Real : s1 > s } as Subset of (TOP-REAL 2) by Lm6;

assume P = { |[r,s]| where r, s is Real : s1 <= s } ; :: thesis: P is closed

then A1: P = P1 ` by Th9;

P1 is open by JORDAN1:23;

hence P is closed by A1, TOPS_1:4; :: thesis: verum