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