:: deftheorem defines ++ MEMBER_1:def 5 :
for F, G being ext-real-membered set holds F ++ G = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ;