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