let X1, X2, Y1, Y2 be set ; :: thesis: [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
A1: [:Y1,X2:] /\ [:X1,Y2:] = [:(Y1 /\ X1),(X2 /\ Y2):] by Th123;
( Y1 /\ X1 c= Y1 & X2 /\ Y2 c= Y2 ) by XBOOLE_1:17;
then A2: [:(Y1 /\ X1),(X2 /\ Y2):] c= [:Y1,Y2:] by Th119;
A3: [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] c= [:X1,X2:] \ [:Y1,Y2:]

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] )

A4: now

assume z in [:(X1 \ Y1),X2:] ; :: thesis: ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] )
then consider x, y being set such that
A5: x in X1 \ Y1 and
A6: y in X2 and
A7: z = [x,y] by Def2;
not x in Y1 by A5, XBOOLE_0:def 5;
then A8: not z in [:Y1,Y2:] by A7, Lm17;
x in X1 by A5, XBOOLE_0:def 5;
then z in [:X1,X2:] by A6, A7, Lm17;
hence ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] ) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

A9: now

assume z in [:X1,(X2 \ Y2):] ; :: thesis: ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] )
then consider x, y being set such that
A10: x in X1 and
A11: y in X2 \ Y2 and
A12: z = [x,y] by Def2;
not y in Y2 by A11, XBOOLE_0:def 5;
then A13: not z in [:Y1,Y2:] by A12, Lm17;
y in X2 by A11, XBOOLE_0:def 5;
then z in [:X1,X2:] by A10, A12, Lm17;
hence ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] ) by A13, XBOOLE_0:def 5; :: thesis: verum

end;

assume z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] ; :: thesis: z in [:X1,X2:] \ [:Y1,Y2:]
hence z in [:X1,X2:] \ [:Y1,Y2:] by A4, A9, XBOOLE_0:def 3; :: thesis: verum

end;

( [:(X1 \ Y1),X2:] = [:X1,X2:] \ [:Y1,X2:] & [:X1,(X2 \ Y2):] = [:X1,X2:] \ [:X1,Y2:] ) by Th125;
then [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] = [:X1,X2:] \ [:(Y1 /\ X1),(X2 /\ Y2):] by A1, XBOOLE_1:54;
then [:X1,X2:] \ [:Y1,Y2:] c= [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by A2, XBOOLE_1:34;
hence [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by A3, XBOOLE_0:def 10; :: thesis: verum