let A, B, C, D be set ; :: thesis: union {A,B,C,D} = ((A \/ B) \/ C) \/ D

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ((A \/ B) \/ C) \/ D c= union {A,B,C,D}

let x be set ; :: thesis: ( x in union {A,B,C,D} implies x in ((A \/ B) \/ C) \/ D )
assume x in union {A,B,C,D} ; :: thesis: x in ((A \/ B) \/ C) \/ D
then consider Z being set such that
A1: x in Z and
A2: Z in {A,B,C,D} by TARSKI:def 4;
( Z = A or Z = B or Z = C or Z = D ) by A2, ENUMSET1:def 2;
hence x in ((A \/ B) \/ C) \/ D by A1, Lm3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((A \/ B) \/ C) \/ D or x in union {A,B,C,D} )
assume x in ((A \/ B) \/ C) \/ D ; :: thesis: x in union {A,B,C,D}
then A3: ( x in A or x in B or x in C or x in D ) by Lm3;
( A in {A,B,C,D} & B in {A,B,C,D} & C in {A,B,C,D} & D in {A,B,C,D} ) by ENUMSET1:def 2;
hence x in union {A,B,C,D} by A3, TARSKI:def 4; :: thesis: verum