let X, Y be ext-real-membered set ; :: thesis: ( X c= Y implies for x being ExtReal st x in SetMajorant Y holds

x in SetMajorant X )

assume A1: X c= Y ; :: thesis: for x being ExtReal st x in SetMajorant Y holds

x in SetMajorant X

let x be ExtReal; :: thesis: ( x in SetMajorant Y implies x in SetMajorant X )

assume x in SetMajorant Y ; :: thesis: x in SetMajorant X

then x is UpperBound of Y by Def1;

then x is UpperBound of X by A1, XXREAL_2:6;

hence x in SetMajorant X by Def1; :: thesis: verum

x in SetMajorant X )

assume A1: X c= Y ; :: thesis: for x being ExtReal st x in SetMajorant Y holds

x in SetMajorant X

let x be ExtReal; :: thesis: ( x in SetMajorant Y implies x in SetMajorant X )

assume x in SetMajorant Y ; :: thesis: x in SetMajorant X

then x is UpperBound of Y by Def1;

then x is UpperBound of X by A1, XXREAL_2:6;

hence x in SetMajorant X by Def1; :: thesis: verum