:: deftheorem Def4 defines INF SUPINF_1:def 4 :
for F being bool_DOMAIN of ExtREAL
for b₂ being ext-real-membered set holds
( b₂ = INF F iff for a being ExtReal holds
( a in b₂ iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) );