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