let A, B, C be set ; :: thesis: (A /\ B) \ C = (A \ C) /\ (B \ C)
A1: A \ C misses C by XBOOLE_1:79;
thus (A /\ B) \ C = (A \ C) /\ B by XBOOLE_1:49
.= (A \ C) \ ((A \ C) \ B) by XBOOLE_1:48
.= (A \ C) \ (A \ (C \/ B)) by XBOOLE_1:41
.= ((A \ C) \ A) \/ ((A \ C) /\ (C \/ B)) by XBOOLE_1:52
.= {} \/ ((A \ C) /\ (C \/ B)) by XBOOLE_1:37
.= (A \ C) /\ ((B \ C) \/ C) by XBOOLE_1:39
.= ((A \ C) /\ (B \ C)) \/ ((A \ C) /\ C) by XBOOLE_1:23
.= ((A \ C) /\ (B \ C)) \/ {} by A1, XBOOLE_0:def 7
.= (A \ C) /\ (B \ C) ; :: thesis: verum