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