let X1, X2, X3, X4 be set ; :: thesis: (X1 \ X2) \ (X3 \ X4) = (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)

assume t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) ; :: thesis: t in (X1 \ X2) \ (X3 \ X4)

then ( t in X1 \ (X2 \/ X3) or t in (X1 /\ X4) \ X2 ) by XBOOLE_0:def 3;

then ( ( t in X1 & not t in X2 \/ X3 ) or ( t in X1 /\ X4 & not t in X2 ) ) by XBOOLE_0:def 5;

then ( ( t in X1 & not t in X2 & not t in X3 ) or ( t in X1 & t in X4 & not t in X2 ) ) by XBOOLE_0:def 3, XBOOLE_0:def 4;

then ( t in X1 \ X2 & not t in X3 \ X4 ) by XBOOLE_0:def 5;

hence t in (X1 \ X2) \ (X3 \ X4) by XBOOLE_0:def 5; :: thesis: verum

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) c= (X1 \ X2) \ (X3 \ X4)

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) or t in (X1 \ X2) \ (X3 \ X4) )let t be object ; :: thesis: ( t in (X1 \ X2) \ (X3 \ X4) implies t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) )

assume t in (X1 \ X2) \ (X3 \ X4) ; :: thesis: t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)

then ( t in X1 \ X2 & not t in X3 \ X4 ) by XBOOLE_0:def 5;

then ( t in X1 & not t in X2 & ( not t in X3 or t in X4 ) ) by XBOOLE_0:def 5;

then ( ( t in X1 & not t in X2 & not t in X3 ) or ( t in X1 /\ X4 & not t in X2 ) ) by XBOOLE_0:def 4;

then ( ( t in X1 & not t in X2 \/ X3 ) or t in (X1 /\ X4) \ X2 ) by XBOOLE_0:def 3, XBOOLE_0:def 5;

then ( t in X1 \ (X2 \/ X3) or t in (X1 /\ X4) \ X2 ) by XBOOLE_0:def 5;

hence t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) by XBOOLE_0:def 3; :: thesis: verum

end;assume t in (X1 \ X2) \ (X3 \ X4) ; :: thesis: t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)

then ( t in X1 \ X2 & not t in X3 \ X4 ) by XBOOLE_0:def 5;

then ( t in X1 & not t in X2 & ( not t in X3 or t in X4 ) ) by XBOOLE_0:def 5;

then ( ( t in X1 & not t in X2 & not t in X3 ) or ( t in X1 /\ X4 & not t in X2 ) ) by XBOOLE_0:def 4;

then ( ( t in X1 & not t in X2 \/ X3 ) or t in (X1 /\ X4) \ X2 ) by XBOOLE_0:def 3, XBOOLE_0:def 5;

then ( t in X1 \ (X2 \/ X3) or t in (X1 /\ X4) \ X2 ) by XBOOLE_0:def 5;

hence t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) by XBOOLE_0:def 3; :: thesis: verum

assume t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) ; :: thesis: t in (X1 \ X2) \ (X3 \ X4)

then ( t in X1 \ (X2 \/ X3) or t in (X1 /\ X4) \ X2 ) by XBOOLE_0:def 3;

then ( ( t in X1 & not t in X2 \/ X3 ) or ( t in X1 /\ X4 & not t in X2 ) ) by XBOOLE_0:def 5;

then ( ( t in X1 & not t in X2 & not t in X3 ) or ( t in X1 & t in X4 & not t in X2 ) ) by XBOOLE_0:def 3, XBOOLE_0:def 4;

then ( t in X1 \ X2 & not t in X3 \ X4 ) by XBOOLE_0:def 5;

hence t in (X1 \ X2) \ (X3 \ X4) by XBOOLE_0:def 5; :: thesis: verum