A: for s being real number st s in X holds
s >= inf X by XXREAL_2:3;

now

let t be real number ; :: thesis: ( ( for s being real number st s in X holds
s >= t ) implies inf X >= t )
assume Z: for s being real number st s in X holds
s >= t ; :: thesis: inf X >= t
for x being ext-real number st x in X holds
t <= x by Z;
then t is LowerBound of X by XXREAL_2:def 2;
hence inf X >= t by XXREAL_2:def 4; :: thesis: verum

end;

hence lower_bound X = inf X by A, Lm61; :: thesis: verum