:: deftheorem Def3 defines SUP SUPINF_1:def 3 :
for F being bool_DOMAIN of ExtREAL
for b₂ being ext-real-membered set holds
( b₂ = SUP 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 = sup A ) ) );