let x, y be ExtReal; :: thesis: for A being ext-real-membered set st y <= x & x is LowerBound of A holds
y is LowerBound of A
let A be ext-real-membered set ; :: thesis: ( y <= x & x is LowerBound of A implies y is LowerBound of A )
assume that
A1: y <= x and
A2: x is LowerBound of A ; :: thesis: y is LowerBound of A
let z be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( z in A implies y <= z )
assume z in A ; :: thesis: y <= z
then x <= z by A2, Def2;
hence y <= z by A1, XXREAL_0:2; :: thesis: verum