defpred S1[ ext-real number ] means $1 in X;
defpred S2[ ext-real number ] means $1 is UpperBound of X;
A:
for r, s being ext-real number st S1[r] & S2[s] holds
r <= s
by Def1;
consider s being ext-real number such that
W1:
for r being ext-real number st S1[r] holds
r <= s
and
W2:
for r being ext-real number st S2[r] holds
s <= r
from XXREAL_1:sch 1(A);
take
s
; :: thesis: ( s is UpperBound of X & ( for x being UpperBound of X holds s <= x ) )
thus
s is UpperBound of X
by W1, Def1; :: thesis: for x being UpperBound of X holds s <= x
thus
for x being UpperBound of X holds s <= x
by W2; :: thesis: verum