:: deftheorem defines -- MEMBER_1:def 15 :
for F being ext-real-membered set
for f being ExtReal holds f -- F = {f} -- F;