for X, Y being ext-real-membered set st X c= Y holds
for x being ExtReal st x in SetMinorant Y holds
x in SetMinorant X