let a, Z1, Z2, Z3 be set ; :: thesis: ( a in (Z1 \/ Z2) \/ Z3 iff ( a in Z1 or a in Z2 or a in Z3 ) )
( a in (Z1 \/ Z2) \/ Z3 iff ( a in Z1 \/ Z2 or a in Z3 ) ) by XBOOLE_0:def 3;
hence ( a in (Z1 \/ Z2) \/ Z3 iff ( a in Z1 or a in Z2 or a in Z3 ) ) by XBOOLE_0:def 3; :: thesis: verum