let X, Y, Z, x be set ; :: thesis: ( x in (X \/ Y) \/ Z iff ( x in X or x in Y or x in Z ) )
set W = (X \/ Y) \/ Z;
( x in (X \/ Y) \/ Z iff ( x in X \/ Y or x in Z ) ) by XBOOLE_0:def 3;
hence ( x in (X \/ Y) \/ Z iff ( x in X or x in Y or x in Z ) ) by XBOOLE_0:def 3; :: thesis: verum