let F, G, H be ext-real-membered set ; :: thesis: F ++ (G /\ H) c= (F ++ G) /\ (F ++ H)
let j be ExtReal; :: 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 H by A3, XBOOLE_0:def 4;
then A4: w + w1 in F ++ H by A2;
w1 in G by A3, XBOOLE_0:def 4;
then w + w1 in F ++ G by A2;
hence j in (F ++ G) /\ (F ++ H) by A1, A4, XBOOLE_0:def 4; :: thesis: verum