let X1, X2, X3, X4 be set ; :: thesis: ( ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ ((X2 \/ X3) \/ X4)) is empty & ((X1 /\ X4) \ (X2 \/ X3)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty & (X1 \ ((X2 \/ X3) \/ X4)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty )
thus ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ ((X2 \/ X3) \/ X4)) is empty :: thesis: ( ((X1 /\ X4) \ (X2 \/ X3)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty & (X1 \ ((X2 \/ X3) \/ X4)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty )
proof
let t be object ; :: according to XBOOLE_0:def 1 :: thesis: not t in ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ ((X2 \/ X3) \/ X4))
assume t in ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ ((X2 \/ X3) \/ X4)) ; :: thesis: contradiction
then ( t in (X1 /\ X4) \ (X2 \/ X3) & t in X1 \ ((X2 \/ X3) \/ X4) ) by XBOOLE_0:def 4;
then ( t in X1 /\ X4 & not t in X2 \/ X3 & t in X1 & not t in (X2 \/ X3) \/ X4 ) by XBOOLE_0:def 5;
then ( t in X1 & t in X4 & ( not t in X2 or not t in X3 ) & t in X1 & not t in X2 & not t in X3 & not t in X4 ) by XBOOLE_0:def 3, XBOOLE_0:def 4;
hence contradiction ; :: thesis: verum
end;
thus ((X1 /\ X4) \ (X2 \/ X3)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty :: thesis: (X1 \ ((X2 \/ X3) \/ X4)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty
proof
let t be object ; :: according to XBOOLE_0:def 1 :: thesis: not t in ((X1 /\ X4) \ (X2 \/ X3)) /\ (((X1 /\ X3) /\ X4) \ X2)
assume t in ((X1 /\ X4) \ (X2 \/ X3)) /\ (((X1 /\ X3) /\ X4) \ X2) ; :: thesis: contradiction
then ( t in (X1 /\ X4) \ (X2 \/ X3) & t in ((X1 /\ X3) /\ X4) \ X2 ) by XBOOLE_0:def 4;
then ( t in X1 /\ X4 & not t in X2 \/ X3 & t in (X1 /\ X3) /\ X4 & not t in X2 ) by XBOOLE_0:def 5;
then ( t in X1 & t in X4 & not t in X2 & not t in X3 & t in X1 /\ X3 & t in X4 & not t in X2 ) by XBOOLE_0:def 3, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 4; :: thesis: verum
end;
let t be object ; :: according to XBOOLE_0:def 1 :: thesis: not t in (X1 \ ((X2 \/ X3) \/ X4)) /\ (((X1 /\ X3) /\ X4) \ X2)
assume t in (X1 \ ((X2 \/ X3) \/ X4)) /\ (((X1 /\ X3) /\ X4) \ X2) ; :: thesis: contradiction
then ( t in X1 \ ((X2 \/ X3) \/ X4) & t in ((X1 /\ X3) /\ X4) \ X2 ) by XBOOLE_0:def 4;
then ( t in X1 & not t in (X2 \/ X3) \/ X4 & t in (X1 /\ X3) /\ X4 & not t in X2 ) by XBOOLE_0:def 5;
then ( t in X1 & not t in X2 \/ X3 & not t in X4 & t in X1 /\ X3 & t in X4 & not t in X2 ) by XBOOLE_0:def 3, XBOOLE_0:def 4;
hence contradiction ; :: thesis: verum