let x, X1, X2, X3, X4 be set ; :: thesis: ( x in ((X1 \/ X2) \/ X3) \/ X4 iff ( x in X1 or x in X2 or x in X3 or x in X4 ) )
set W = ((X1 \/ X2) \/ X3) \/ X4;
( x in ((X1 \/ X2) \/ X3) \/ X4 iff ( x in (X1 \/ X2) \/ X3 or x in X4 ) ) by XBOOLE_0:def 3;
hence ( x in ((X1 \/ X2) \/ X3) \/ X4 iff ( x in X1 or x in X2 or x in X3 or x in X4 ) ) by LmSTC0IS7a; :: thesis: verum