let x be ExtReal; :: thesis: for A being ext-real-membered set st x in A holds
inf A <= x
let A be ext-real-membered set ; :: thesis: ( x in A implies inf A <= x )
inf A is LowerBound of A by Def4;
hence ( x in A implies inf A <= x ) by Def2; :: thesis: verum