set A = the Element of F;

defpred S_{1}[ 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_{1}[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

defpred S

( 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

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