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 = inf Y )
let Y be non empty Subset of REAL ; :: thesis: ( X = Y & Y is bounded_below implies ( X is bounded_below & inf X = inf Y ) )
assume A1: ( X = Y & Y is bounded_below ) ; :: thesis: ( X is bounded_below & inf X = inf Y )
for r being ext-real number st r in X holds
inf Y <= r by A1, SEQ_4:def 5;
then A3: lower_bound Y is LowerBound of X by XXREAL_2:def 2;
hence A4: X is bounded_below by SUPINF_1:def 12; :: thesis: inf X = inf Y
A5: inf Y <= inf X by A3, XXREAL_2:def 4;
not +infty in X by A1;
then X <> {+infty } by TARSKI:def 1;
then B6: inf X in REAL by A4, XXREAL_2:58;
for s being real number st s in Y holds
inf X <= s by A1, XXREAL_2:3;
then inf X <= inf Y by B6, SEQ_4:60;
hence inf X = inf Y by A5, XXREAL_0:1; :: thesis: verum