let X, Y be ext-real-membered set ; :: thesis: ( ( for y being ExtReal st y in Y holds

ex x being ExtReal st

( x in X & x <= y ) ) implies inf X <= inf Y )

assume A1: for y being ExtReal st y in Y holds

ex x being ExtReal st

( x in X & x <= y ) ; :: thesis: inf X <= inf Y

inf X is LowerBound of Y

ex x being ExtReal st

( x in X & x <= y ) ) implies inf X <= inf Y )

assume A1: for y being ExtReal st y in Y holds

ex x being ExtReal st

( x in X & x <= y ) ; :: thesis: inf X <= inf Y

inf X is LowerBound of Y

proof

hence
inf X <= inf Y
by Def4; :: thesis: verum
let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( y in Y implies inf X <= y )

assume y in Y ; :: thesis: inf X <= y

then consider x being ExtReal such that

A2: x in X and

A3: x <= y by A1;

inf X <= x by A2, Th3;

hence inf X <= y by A3, XXREAL_0:2; :: thesis: verum

end;assume y in Y ; :: thesis: inf X <= y

then consider x being ExtReal such that

A2: x in X and

A3: x <= y by A1;

inf X <= x by A2, Th3;

hence inf X <= y by A3, XXREAL_0:2; :: thesis: verum