let G1, G2 be non empty Subset of ExtREAL ; :: thesis: ( ( for y being R_eal holds
( y in G1 iff ( 0. < y & y + y < x ) ) ) & ( for y being R_eal holds
( y in G2 iff ( 0. < y & y + y < x ) ) ) implies G1 = G2 )
assume that
A5: for y being R_eal holds
( y in G1 iff ( 0. < y & y + y < x ) ) and
A6: for y being R_eal holds
( y in G2 iff ( 0. < y & y + y < x ) ) ; :: thesis: G1 = G2
thus G1 c= G2 :: according to XBOOLE_0:def 10 :: thesis: G2 c= G1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in G1 or y in G2 )
assume A7: y in G1 ; :: thesis: y in G2
then reconsider y = y as R_eal ;
( 0. < y & y + y < x ) by A5, A7;
hence y in G2 by A6; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in G2 or y in G1 )
assume A8: y in G2 ; :: thesis: y in G1
then reconsider y = y as R_eal ;
( 0. < y & y + y < x ) by A6, A8;
hence y in G1 by A5; :: thesis: verum