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

proof

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;

hence inf X <= inf Y by Def4; :: thesis: verum