defpred S1[ ext-real number ] means $1 is LowerBound of X;
defpred S2[ ext-real number ] means $1 in X;
A:
for r, s being ext-real number st S1[r] & S2[s] holds
r <= s
by Def2;
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 LowerBound of X & ( for x being LowerBound of X holds x <= s ) )
thus
s is LowerBound of X
by W2, Def2; :: thesis: for x being LowerBound of X holds x <= s
thus
for x being LowerBound of X holds x <= s
by W1; :: thesis: verum