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

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