defpred S₁[ set ] means for y being R_eal st y = $1 holds
( 0. < y & y + y < x );
consider D being set such that
A2: for y being set holds
( y in D iff ( y in ExtREAL & S₁[y] ) ) from XBOOLE_0:sch 1();
A3: for y being R_eal holds
( y in D iff ( 0. < y & y + y < x ) )

proof

let y be R_eal; :: thesis: ( y in D iff ( 0. < y & y + y < x ) )
( 0. < y & y + y < x implies y in D )

proof

assume ( 0. < y & y + y < x ) ; :: thesis: y in D
then for z being R_eal st z = y holds
( 0. < z & z + z < x ) ;
hence y in D by A2; :: thesis: verum

end;

hence ( y in D iff ( 0. < y & y + y < x ) ) by A2; :: thesis: verum

end;

consider y being R_eal such that
A4: ( 0. < y & y + y < x ) by A1, Th26;
for z being set st z in D holds
z in ExtREAL by A2;
then D is non empty Subset of ExtREAL by A3, A4, TARSKI:def 3;
hence ex b₁ being non empty Subset of ExtREAL st
for y being R_eal holds
( y in b₁ iff ( 0. < y & y + y < x ) ) by A3; :: thesis: verum