let F, G, H be ext-real-membered set ; :: thesis: F ++ (G /\ H) c= (F ++ G) /\ (F ++ H)
let j be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not j in F ++ (G /\ H) or j in (F ++ G) /\ (F ++ H) )
assume j in F ++ (G /\ H) ; :: thesis: j in (F ++ G) /\ (F ++ H)
then consider w, w1 being Element of ExtREAL such that
A1: j = w + w1 and
A2: w in F and
A3: w1 in G /\ H ;
( w1 in G & w1 in H ) by A3, XBOOLE_0:def 4;
then ( w + w1 in F ++ G & w + w1 in F ++ H ) by A2;
hence j in (F ++ G) /\ (F ++ H) by A1, XBOOLE_0:def 4; :: thesis: verum