defpred S1[ object ] means $1 in X;
defpred S2[ object ] means $1 is LowerBound of X;
A9: for r, s being ExtReal st S2[r] & S1[s] holds
r <= s by Def2;
consider s being ExtReal such that
A10: for r being ExtReal st S2[r] holds
r <= s and
A11: for r being ExtReal st S1[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