let s be real number ; :: thesis: [.s,+infty .[ = { g where g is Real : s <= g }
thus [.s,+infty .[ c= { g where g is Real : s <= g } :: according to XBOOLE_0:def 10 :: thesis: { g where g is Real : s <= g } c= [.s,+infty .[

proof

let x be real number ; :: according to MEMBERED:def 9 :: thesis: ( not x in [.s,+infty .[ or x in { g where g is Real : s <= g } )
assume x in [.s,+infty .[ ; :: thesis: x in { g where g is Real : s <= g }
then A1: s <= x by Th3;
x in REAL by XREAL_0:def 1;
hence x in { g where g is Real : s <= g } by A1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Real : s <= g } or x in [.s,+infty .[ )
assume x in { g where g is Real : s <= g } ; :: thesis: x in [.s,+infty .[
then consider g being Real such that
A2: x = g and
A3: s <= g ;
g < +infty by XXREAL_0:9;
hence x in [.s,+infty .[ by A2, A3, Th3; :: thesis: verum