set A = the Element of F;
defpred S₁[ ExtReal] means ex A being non empty ext-real-membered set st
( A in F & $1 = inf A );
reconsider A = the Element of F as non empty ext-real-membered set by SETFAM_1:def 8;
consider S being ext-real-membered set such that
A1: for a being ExtReal holds
( a in S iff S₁[a] ) from MEMBERED:sch 2();
inf A = inf A ;
then reconsider S = S as non empty ext-real-membered set by A1;
take S ; :: thesis: for a being ExtReal 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 ExtReal holds
( a in S iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) by A1; :: thesis: verum