let s be ext-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 A1: x in ].s,+infty.[ ; :: thesis: x in { g where g is Real : s < g }
then A2: s < x by Th4;
x < +infty by A1, Th4;
then x in REAL by A2, XXREAL_0:48;
hence x in { g where g is Real : s < g } by A2; :: 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
A3: x = g and
A4: s < g ;
g < +infty by XXREAL_0:9;
hence x in ].s,+infty.[ by A3, A4, Th4; :: thesis: verum