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

consider Y being ext-real-membered set such that

A1: for x being ExtReal holds

( x in Y iff S

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