let X be set ; :: thesis:
let A be Subset of X; :: thesis:
A1: [:(X \ A),X:] \/ [:X,A:] c= [:A,A:] \/ [:(X \ A),X:]

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in [:(X \ A),X:] \/ [:X,A:] ; :: thesis:
[:(X \ A),X:] \/ [:X,A:] c= [:X,X:] by Th2;
then consider a, b being object such that
A3: a in X and
A4: b in X and
A5: x = [a,b] by A2, ZFMISC_1:def 2;

suppose A6: a in A ; :: thesis:

assume not x in [:X,A:] ; :: thesis:
then x in [:(X \ A),X:] by A2, XBOOLE_0:def 3;
then ( a in X \ A & b in X ) by A5, ZFMISC_1:87;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis:

end;

then b in A by A5, ZFMISC_1:87;
then A7: x in [:A,A:] by A6, A5, ZFMISC_1:87;
[:A,A:] c= [:A,A:] \/ [:(X \ A),X:] by XBOOLE_1:7;
hence x in [:A,A:] \/ [:(X \ A),X:] by A7; :: thesis:

end;

suppose not a in A ; :: thesis:

then a in X \ A by A3, XBOOLE_0:def 5;
then A8: x in [:(X \ A),X:] by A4, A5, ZFMISC_1:87;
[:(X \ A),X:] c= [:(X \ A),X:] \/ [:A,A:] by XBOOLE_1:7;
hence x in [:A,A:] \/ [:(X \ A),X:] by A8; :: thesis:

end;

end;

end;

[:A,A:] c= [:X,A:] by ZFMISC_1:95;
hence [:(X \ A),X:] \/ [:X,A:] = [:A,A:] \/ [:(X \ A),X:] by A1, XBOOLE_1:13; :: thesis: