A1: now :: thesis: for t being Real st ( for s being Real st s in X holds
s >= t ) holds
inf X >= t

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

end;

for s being Real st s in X holds
s >= inf X by XXREAL_2:3;
hence lower_bound X = inf X by A1, Lm1; :: thesis: verum