let X be ext-real-membered set ; :: thesis: for x being ExtReal st ex y being ExtReal st
( y in X & y <= x ) holds
inf X <= x
let x be ExtReal; :: thesis: ( ex y being ExtReal st
( y in X & y <= x ) implies inf X <= x )
given y being ExtReal such that A1: y in X and
A2: y <= x ; :: thesis: inf X <= x
inf X <= y by A1, Th3;
hence inf X <= x by A2, XXREAL_0:2; :: thesis: verum