let X, Y be ext-real-membered set ; :: thesis: ( X c= Y implies for x being ext-real number st x in SetMajorant Y holds
x in SetMajorant X )
assume A1: X c= Y ; :: thesis: for x being ext-real number st x in SetMajorant Y holds
x in SetMajorant X
let x be ext-real number ; :: 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 Def14;
then x is UpperBound of X by A1, XXREAL_2:6;
hence x in SetMajorant X by Def14; :: thesis: verum