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

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 ; :: 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;

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) )
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