let A, B, C be complex-membered set ; (A ++ B) ++ C = A ++ (B ++ C)
let a be Complex; MEMBERED:def 13 ( ( 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 ( not a in A ++ (B ++ C) or a in (A ++ B) ++ C )
assume
a in (A ++ B) ++ C
;
a in A ++ (B ++ C)then consider c,
c1 being
Complex such that A1:
a = c + c1
and A2:
c in A ++ B
and A3:
c1 in C
;
consider c2,
c3 being
Complex such that A4:
c = c2 + c3
and A5:
c2 in A
and A6:
c3 in B
by A2;
(
a = c2 + (c3 + c1) &
c3 + c1 in B ++ C )
by A1, A3, A4, A6;
hence
a in A ++ (B ++ C)
by A5;
verum
end;
assume
a in A ++ (B ++ C)
; a in (A ++ B) ++ C
then consider c, c1 being Complex such that
A7:
( a = c + c1 & c in A )
and
A8:
c1 in B ++ C
;
consider c2, c3 being Complex such that
A9:
( c1 = c2 + c3 & c2 in B )
and
A10:
c3 in C
by A8;
( a = (c + c2) + c3 & c + c2 in A ++ B )
by A7, A9;
hence
a in (A ++ B) ++ C
by A10; verum