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

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