let X1, X2, Y1, Y2 be set ; :: thesis: [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
( [:(X1 \ Y1),X2:] = [:X1,X2:] \ [:Y1,X2:] & [:X1,(X2 \ Y2):] = [:X1,X2:] \ [:X1,Y2:] & [:Y1,X2:] /\ [:X1,Y2:] = [:(Y1 /\ X1),(X2 /\ Y2):] & Y1 /\ X1 c= Y1 & X2 /\ Y2 c= Y2 ) by Th123, Th125, XBOOLE_1:17;
then ( [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] = [:X1,X2:] \ [:(Y1 /\ X1),(X2 /\ Y2):] & [:(Y1 /\ X1),(X2 /\ Y2):] c= [:Y1,Y2:] ) by Th119, XBOOLE_1:54;
then A1: [:X1,X2:] \ [:Y1,Y2:] c= [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by XBOOLE_1:34;
[:(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:] )
assume A2: z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] ; :: thesis: z in [:X1,X2:] \ [:Y1,Y2:]

A3: now

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

end;

now

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

end;

hence z in [:X1,X2:] \ [:Y1,Y2:] by A2, A3, XBOOLE_0:def 3; :: thesis: verum

end;

hence [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by A1, XBOOLE_0:def 10; :: thesis: verum