let F be bool_DOMAIN of ExtREAL; :: thesis: for S being ext-real-membered set st S = union F holds
inf (INF F) is LowerBound of S
let S be ext-real-membered set ; :: thesis: ( S = union F implies inf (INF F) is LowerBound of S )
assume A1: S = union F ; :: thesis: inf (INF F) is LowerBound of S
for x being ext-real number st x in S holds
inf (INF F) <= x

proof

let x be ext-real number ; :: thesis: ( x in S implies inf (INF F) <= x )
assume x in S ; :: thesis: inf (INF F) <= x
then consider Z being set such that
A2: x in Z and
A3: Z in F by A1, TARSKI:def 4;
reconsider Z = Z as non empty ext-real-membered set by A2, A3;
consider a being set such that
A4: a = inf Z ;
reconsider a = a as ext-real number by A4;
( inf Z is LowerBound of Z & a in INF F ) by A3, A4, Def20, XXREAL_2:def 4;
hence inf (INF F) <= x by A2, A4, XXREAL_2:62, XXREAL_2:def 2; :: thesis: verum

end;

hence inf (INF F) is LowerBound of S by XXREAL_2:def 2; :: thesis: verum