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

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

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

r <= s by Def2;

consider s being ExtReal such that

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

r <= s and

A11: for r being ExtReal st S_{1}[r] holds

s <= r from XXREAL_1:sch 1(A9);

take s ; :: thesis: ( s is LowerBound of X & ( for x being LowerBound of X holds x <= s ) )

thus s is LowerBound of X by A11, Def2; :: thesis: for x being LowerBound of X holds x <= s

thus for x being LowerBound of X holds x <= s by A10; :: thesis: verum

defpred S

A9: for r, s being ExtReal st S

r <= s by Def2;

consider s being ExtReal such that

A10: for r being ExtReal st S

r <= s and

A11: for r being ExtReal st S

s <= r from XXREAL_1:sch 1(A9);

take s ; :: thesis: ( s is LowerBound of X & ( for x being LowerBound of X holds x <= s ) )

thus s is LowerBound of X by A11, Def2; :: thesis: for x being LowerBound of X holds x <= s

thus for x being LowerBound of X holds x <= s by A10; :: thesis: verum