defpred S1[ object ] means $1 is UpperBound of X;
defpred S2[ object ] means $1 in X;
A1: for r, s being ExtReal st S2[r] & S1[s] holds
r <= s by Def1;
consider s being ExtReal such that
A2: for r being ExtReal st S2[r] holds
r <= s and
A3: for r being ExtReal st S1[r] holds
s <= r from XXREAL_1:sch 1(A1);
 take s ; :: thesis: ( s is UpperBound of X & ( for x being UpperBound of X holds s <= x ) )
thus s is UpperBound of X by A2, Def1; :: thesis: for x being UpperBound of X holds s <= x
thus for x being UpperBound of X holds s <= x by A3; :: thesis: verum