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