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