let F be bool_DOMAIN of ExtREAL ; :: thesis: for S being non empty ext-real-membered set st S = union F holds
inf S = inf (INF F)
let S be non empty ext-real-membered set ; :: thesis: ( S = union F implies inf S = inf (INF F) )
assume A1: S = union F ; :: thesis: inf S = inf (INF F)
set a = inf S;
set b = inf (INF F);
A2: inf (INF F) is LowerBound of S by A1, Th118;
inf S is LowerBound of INF F by A1, Th117;
then ( inf S <= inf (INF F) & inf (INF F) <= inf S ) by A2, XXREAL_2:def 4;
hence inf S = inf (INF F) by XXREAL_0:1; :: thesis: verum