defpred S₁[ ExtReal] means $1 is LowerBound of X;
consider Y being ext-real-membered set such that
A1: for x being ExtReal holds
( x in Y iff S₁[x] ) from MEMBERED:sch 2();
take Y ; :: thesis: for x being ExtReal holds
( x in Y iff x is LowerBound of X )
thus for x being ExtReal holds
( x in Y iff x is LowerBound of X ) by A1; :: thesis: verum