defpred S_{1}[ ExtReal] means $1 is UpperBound 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 UpperBound of X )

thus for x being ExtReal holds

( x in Y iff x is UpperBound 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 UpperBound of X )

thus for x being ExtReal holds

( x in Y iff x is UpperBound of X ) by A1; :: thesis: verum