:: deftheorem defines -- MEMBER_1:def 1 :
for F being ext-real-membered set holds -- F = { (- w) where w is Element of ExtREAL : w in F } ;