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