defpred S_{1}[ object ] means $1 is UpperBound of X;

defpred S_{2}[ object ] means $1 in X;

A1: for r, s being ExtReal st S_{2}[r] & S_{1}[s] holds

r <= s by Def1;

consider s being ExtReal such that

A2: for r being ExtReal st S_{2}[r] holds

r <= s and

A3: for r being ExtReal st S_{1}[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

defpred S

A1: for r, s being ExtReal st S

r <= s by Def1;

consider s being ExtReal such that

A2: for r being ExtReal st S

r <= s and

A3: for r being ExtReal st S

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