let X, Y be ext-real-membered set ; :: thesis: ( X c= Y implies for x being ext-real number st x in SetMinorant Y holds
x in SetMinorant X )
assume A1: X c= Y ; :: thesis: for x being ext-real number st x in SetMinorant Y holds
x in SetMinorant X
let x be ext-real number ; :: thesis: ( x in SetMinorant Y implies x in SetMinorant X )
assume x in SetMinorant Y ; :: thesis: x in SetMinorant X
then x is LowerBound of Y by Def15;
then x is LowerBound of X by A1, XXREAL_2:5;
hence x in SetMinorant X by Def15; :: thesis: verum