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