let A, B, C, D be set ; :: thesis: union {A,B,C,D} = ((A \/ B) \/ C) \/ D
A1: B in {A,B,C,D} by ENUMSET1:def 2;
A2: D in {A,B,C,D} by ENUMSET1:def 2;

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

let x be object ; :: 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
A3: x in Z and
A4: Z in {A,B,C,D} by TARSKI:def 4;
( Z = A or Z = B or Z = C or Z = D ) by A4, ENUMSET1:def 2;
hence x in ((A \/ B) \/ C) \/ D by A3, Lm3; :: thesis: verum

end;

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