for X, Y being ext-real-membered set st ( for y being ExtReal st y in Y holds
ex x being ExtReal st
( x in X & x <= y ) ) holds
inf X <= inf Y