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