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

x in SetMinorant X )

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

x in SetMinorant X

let x be ExtReal; :: 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 Def2;

then x is LowerBound of X by A1, XXREAL_2:5;

hence x in SetMinorant X by Def2; :: thesis: verum

x in SetMinorant X )

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

x in SetMinorant X

let x be ExtReal; :: 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 Def2;

then x is LowerBound of X by A1, XXREAL_2:5;

hence x in SetMinorant X by Def2; :: thesis: verum