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

( 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