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 Th99;
( Y1 /\ X1 c= Y1 & X2 /\ Y2 c= Y2 ) by XBOOLE_1:17;
then A2: [:(Y1 /\ X1),(X2 /\ Y2):] c= [:Y1,Y2:] by Th95;
A3: [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] c= [:X1,X2:] \ [:Y1,Y2:]
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or z in [:X1,X2:] \ [:Y1,Y2:] )
A4: now :: thesis: ( z in [:(X1 \ Y1),X2:] & z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] implies z in [:X1,X2:] \ [:Y1,Y2:] )
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 object 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, Lm16;
x in X1 by A5, XBOOLE_0:def 5;
then z in [:X1,X2:] by A6, A7, Lm16;
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 :: thesis: ( z in [:X1,(X2 \ Y2):] & z in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] implies z in [:X1,X2:] \ [:Y1,Y2:] )
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 object 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, Lm16;
y in X2 by A11, XBOOLE_0:def 5;
then z in [:X1,X2:] by A10, A12, Lm16;
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 Th101;
then [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] = [:X1,X2:] \ [:(Y1 /\ X1),(X2 /\ Y2):] by A1, XBOOLE_1:54;
hence [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by A3, A2, XBOOLE_1:34; :: thesis: verum