let e be object ; :: according to MEMBERED:def 2 :: thesis: ( not e in F ** G or e is ext-real )
assume e in F ** G ; :: thesis: e is ext-real
then ex w1, w2 being Element of ExtREAL st
( e = w1 * w2 & w1 in F & w2 in G ) ;
hence e is ext-real ; :: thesis: verum