defpred S₁[ ext-real number ] means ex A being non empty ext-real-membered set st
( A in F & $1 = inf A );
consider A being Element of F;
reconsider A = A as non empty ext-real-membered set by SETFAM_1:def 9;
A1: inf A = inf A ;
consider S being ext-real-membered set such that
A2: for a being ext-real number holds
( a in S iff S₁[a] ) from MEMBERED:sch 2();
reconsider S = S as non empty ext-real-membered set by A1, A2;
take S ; :: thesis: for a being ext-real number holds
( a in S iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) )
thus for a being ext-real number holds
( a in S iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) by A2; :: thesis: verum