let A, B, C be complex-membered set ; :: thesis: (A ++ B) ++ C = A ++ (B ++ C)
let a be complex number ; :: according to MEMBERED:def 13 :: thesis: ( ( not a in (A ++ B) ++ C or a in A ++ (B ++ C) ) & ( not a in A ++ (B ++ C) or a in (A ++ B) ++ C ) )

hereby :: thesis: ( not a in A ++ (B ++ C) or a in (A ++ B) ++ C )

assume a in (A ++ B) ++ C ; :: thesis: a in A ++ (B ++ C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c + c1 and
A2: c in A ++ B and
A3: c1 in C ;
consider c2, c3 being Element of COMPLEX such that
A4: c = c2 + c3 and
A5: c2 in A and
A6: c3 in B by A2;
A7: a = c2 + (c3 + c1) by A1, A4;
c3 + c1 in B ++ C by A6, A3;
hence a in A ++ (B ++ C) by A5, A7; :: thesis: verum

end;

assume a in A ++ (B ++ C) ; :: thesis: a in (A ++ B) ++ C
then consider c, c1 being Element of COMPLEX such that
A8: a = c + c1 and
A9: c in A and
A10: c1 in B ++ C ;
consider c2, c3 being Element of COMPLEX such that
A11: c1 = c2 + c3 and
A12: c2 in B and
A13: c3 in C by A10;
A14: a = (c + c2) + c3 by A8, A11;
c + c2 in A ++ B by A9, A12;
hence a in (A ++ B) ++ C by A13, A14; :: thesis: verum