let F, G, H, I be ext-real-membered set ; :: thesis: ( F c= G & H c= I implies F ** H c= G ** I )
assume A1: ( F c= G & H c= I ) ; :: thesis: F ** H c= G ** I
let i be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not i in F ** H or i in G ** I )
assume i in F ** H ; :: thesis: i in G ** I
then ex w, w1 being Element of ExtREAL st
( i = w * w1 & w in F & w1 in H ) ;
hence i in G ** I by A1; :: thesis: verum