let A, B be ext-real-membered set ; :: thesis: ( B c= A implies for x being UpperBound of A holds x is UpperBound of B )
assume A1: B c= A ; :: thesis: for x being UpperBound of A holds x is UpperBound of B
let x be UpperBound of A; :: thesis: x is UpperBound of B
let y be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( y in B implies y <= x )
assume y in B ; :: thesis: y <= x
hence y <= x by A1, Def1; :: thesis: verum