let X be non empty Subset of ExtREAL; :: thesis: for Y being non empty Subset of REAL st X = Y & Y is bounded_below holds
( X is bounded_below & inf X = lower_bound Y )
let Y be non empty Subset of REAL; :: thesis: ( X = Y & Y is bounded_below implies ( X is bounded_below & inf X = lower_bound Y ) )
assume that
A1: X = Y and
A2: Y is bounded_below ; :: thesis: ( X is bounded_below & inf X = lower_bound Y )
A3: for s being Real st s in Y holds
inf X <= s by A1, XXREAL_2:3;
not +infty in X by A1;
then A4: X <> {+infty} by TARSKI:def 1;
for r being ExtReal st r in X holds
lower_bound Y <= r by A1, A2, SEQ_4:def 2;
then A5: lower_bound Y is LowerBound of X by XXREAL_2:def 2;
hence X is bounded_below by XXREAL_2:def 9; :: thesis: inf X = lower_bound Y
then inf X in REAL by A4, XXREAL_2:58;
then A6: inf X <= lower_bound Y by A3, SEQ_4:43;
lower_bound Y <= inf X by A5, XXREAL_2:def 4;
hence inf X = lower_bound Y by A6, XXREAL_0:1; :: thesis: verum