let x, A, B, C, D be set ; :: thesis: ( x in ((A \/ B) \/ C) \/ D iff ( x in A or x in B or x in C or x in D ) )

hereby :: thesis: ( ( x in A or x in B or x in C or x in D ) implies x in ((A \/ B) \/ C) \/ D )

assume x in ((A \/ B) \/ C) \/ D ; :: thesis: ( x in A or x in B or x in C or x in D )
then ( x in (A \/ B) \/ C or x in D ) by XBOOLE_0:def 3;
then ( x in A \/ B or x in C or x in D ) by XBOOLE_0:def 3;
hence ( x in A or x in B or x in C or x in D ) by XBOOLE_0:def 3; :: thesis: verum

end;

assume ( x in A or x in B or x in C or x in D ) ; :: thesis: x in ((A \/ B) \/ C) \/ D
then ( x in A \/ B or x in C or x in D ) by XBOOLE_0:def 3;
then ( x in (A \/ B) \/ C or x in D ) by XBOOLE_0:def 3;
hence x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def 3; :: thesis: verum