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

( 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