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 )
A2: F /// H = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in H ) } by Th101;
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 ) by A2;
hence i in G /// I by A1, Th102; :: thesis: verum