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

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