let B, A be ext-real-membered set ; :: thesis: ( B c= A implies for x being LowerBound of A holds x is LowerBound of B )
assume Z: 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 ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( y in B implies x <= y )
assume y in B ; :: thesis: x <= y
hence x <= y by Def2, Z; :: thesis: verum