defpred S₁[ ExtReal] means ex A being non empty ext-real-membered set st
( A in F & $1 = sup A );
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();
reconsider S = S as ext-real-membered set ;
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 = sup 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 = sup A ) ) by A1; :: thesis: verum