let A, B, C be complex-membered set ; :: thesis: A ++ (B /\ C) c= (A ++ B) /\ (A ++ C)
let a be Complex; :: according to MEMBERED:def 7 :: thesis: ( not a in A ++ (B /\ C) or a in (A ++ B) /\ (A ++ C) )
assume a in A ++ (B /\ C) ; :: thesis: a in (A ++ B) /\ (A ++ C)
then consider c, c1 being Complex such that
A1: a = c + c1 and
A2: c in A and
A3: c1 in B /\ C ;
c1 in C by A3, XBOOLE_0:def 4;
then A4: c + c1 in A ++ C by A2;
c1 in B by A3, XBOOLE_0:def 4;
then c + c1 in A ++ B by A2;
hence a in (A ++ B) /\ (A ++ C) by A1, A4, XBOOLE_0:def 4; :: thesis: verum