let X be ext-real-membered set ; :: thesis: for x being ext-real number st ex y being ext-real number st
( y in X & y <= x ) holds
inf X <= x
let x be ext-real number ; :: thesis: ( ex y being ext-real number st
( y in X & y <= x ) implies inf X <= x )
given y being ext-real number 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