let A, B be ext-real-membered set ; :: thesis: ( B c= A implies for x being LowerBound of A holds x is LowerBound of B )

assume A1: B c= A ; :: thesis: for x being LowerBound of A holds x is LowerBound of B

let x be LowerBound of A; :: thesis: x is LowerBound of B

let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( y in B implies x <= y )

assume y in B ; :: thesis: x <= y

hence x <= y by A1, Def2; :: thesis: verum

assume A1: B c= A ; :: thesis: for x being LowerBound of A holds x is LowerBound of B

let x be LowerBound of A; :: thesis: x is LowerBound of B

let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( y in B implies x <= y )

assume y in B ; :: thesis: x <= y

hence x <= y by A1, Def2; :: thesis: verum