let X1, X2, Y1, Y2 be set ; :: thesis: ( [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] & [:(X1 \ Y1),X2:] misses [:(X1 /\ Y1),(X2 \ Y2):] )
A2: [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] c= [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] or x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] )
assume A3: x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] ; :: thesis: x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):]
now :: thesis: x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):]
per cases ( x in [:(X1 \ Y1),X2:] or x in [:X1,(X2 \ Y2):] ) by A3, XBOOLE_0:def 3;
suppose x in [:(X1 \ Y1),X2:] ; :: thesis: x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):]
hence x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] by XBOOLE_0:def 3; :: thesis: verum
end;
suppose x in [:X1,(X2 \ Y2):] ; :: thesis: x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):]
then consider x1, x2 being object such that
A4: x1 in X1 and
A5: x2 in X2 \ Y2 and
A6: x = [x1,x2] by ZFMISC_1:def 2;
( ( x1 in X1 & not x1 in Y1 ) or ( x1 in X1 & x1 in Y1 ) ) by A4;
then ( ( x1 in X1 \ Y1 & x2 in X2 ) or ( x1 in X1 /\ Y1 & x2 in X2 \ Y2 ) ) by A5, XBOOLE_0:def 4, XBOOLE_0:def 5;
then ( x in [:(X1 \ Y1),X2:] or x in [:(X1 /\ Y1),(X2 \ Y2):] ) by A6, ZFMISC_1:def 2;
hence x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] ; :: thesis: verum
end;
A7: [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] c= [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] or x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] )
assume A8: x in [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] ; :: thesis: x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
now :: thesis: x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
per cases ( x in [:(X1 \ Y1),X2:] or x in [:(X1 /\ Y1),(X2 \ Y2):] ) by A8, XBOOLE_0:def 3;
suppose x in [:(X1 \ Y1),X2:] ; :: thesis: x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
hence x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by XBOOLE_0:def 3; :: thesis: verum
end;
suppose x in [:(X1 /\ Y1),(X2 \ Y2):] ; :: thesis: x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]
then consider x1, x2 being object such that
A9: x1 in X1 /\ Y1 and
A10: x2 in X2 \ Y2 and
A11: x = [x1,x2] by ZFMISC_1:def 2;
( x1 in X1 & x2 in X2 \ Y2 & x = [x1,x2] ) by A9, A10, A11, XBOOLE_0:def 4;
then x in [:X1,(X2 \ Y2):] by ZFMISC_1:def 2;
hence x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence x in [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):] ; :: thesis: verum
end;
[:(X1 \ Y1),X2:] misses [:(X1 /\ Y1),(X2 \ Y2):]
proof
now :: thesis: for x being object holds not x in [:(X1 \ Y1),X2:] /\ [:(X1 /\ Y1),(X2 \ Y2):]
let x be object ; :: thesis: not x in [:(X1 \ Y1),X2:] /\ [:(X1 /\ Y1),(X2 \ Y2):]
assume x in [:(X1 \ Y1),X2:] /\ [:(X1 /\ Y1),(X2 \ Y2):] ; :: thesis: contradiction
then A12: ( x in [:(X1 \ Y1),X2:] & x in [:(X1 /\ Y1),(X2 \ Y2):] ) by XBOOLE_0:def 4;
then consider a1, a2 being object such that
A13: ( a1 in X1 \ Y1 & a2 in X2 & x = [a1,a2] ) by ZFMISC_1:def 2;
consider a3, a4 being object such that
A14: ( a3 in X1 /\ Y1 & a4 in X2 \ Y2 & x = [a3,a4] ) by ZFMISC_1:def 2, A12;
( a1 = a3 & a2 = a4 ) by XTUPLE_0:1, A13, A14;
then ( a1 in X1 & not a1 in Y1 & a1 in Y1 ) by A13, A14, XBOOLE_0:def 4, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum
end;
then [:(X1 \ Y1),X2:] /\ [:(X1 /\ Y1),(X2 \ Y2):] is empty ;
hence [:(X1 \ Y1),X2:] misses [:(X1 /\ Y1),(X2 \ Y2):] ; :: thesis: verum
end;
hence ( [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] & [:(X1 \ Y1),X2:] misses [:(X1 /\ Y1),(X2 \ Y2):] ) by A2, A7, ZFMISC_1:103; :: thesis: verum