let X1, X2, X3, X4 be set ; :: thesis: (X1 /\ X4) \ X2 c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (X1 /\ X4) \ X2 or t in (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2) )
assume t in (X1 /\ X4) \ X2 ; :: thesis: t in (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
then ( ( t in X1 & t in X4 & not t in X2 & not t in X3 ) or ( t in X1 & not t in X2 & not t in X3 & not t in X4 ) or ( t in X1 & t in X3 & t in X4 & not t in X2 ) ) by XBOOLE_0:def 4, XBOOLE_0:def 5;
then ( ( t in X1 & t in X4 & not t in X2 & not t in X3 ) or ( t in X1 & not t in X2 \/ X3 & not t in X4 ) or ( t in X1 /\ X3 & t in X4 & not t in X2 ) ) by XBOOLE_0:def 3, XBOOLE_0:def 4;
then ( ( t in X1 /\ X4 & not t in X2 \/ X3 ) or ( t in X1 & not t in (X2 \/ X3) \/ X4 ) or ( t in (X1 /\ X3) /\ X4 & not t in X2 ) ) by XBOOLE_0:def 3, XBOOLE_0:def 4;
then ( t in (X1 /\ X4) \ (X2 \/ X3) or t in X1 \ ((X2 \/ X3) \/ X4) or t in ((X1 /\ X3) /\ X4) \ X2 ) by XBOOLE_0:def 5;
then ( t in ((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4)) or t in ((X1 /\ X3) /\ X4) \ X2 ) by XBOOLE_0:def 3;
hence t in (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2) by XBOOLE_0:def 3; :: thesis: verum