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