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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(X \ A),X:] \/ [:X,A:] or x in [:A,A:] \/ [:(X \ A),X:] )
assume A2: x in [:(X \ A),X:] \/ [:X,A:] ; :: thesis: x in [:A,A:] \/ [:(X \ A),X:]
[:(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;

per cases ( a in A or not a in A ) ;

suppose A6: a in A ; :: thesis: x in [:A,A:] \/ [:(X \ A),X:]

x in [:X,A:]

proof

assume not x in [:X,A:] ; :: thesis: contradiction
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: verum

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: verum

end;

suppose not a in A ; :: thesis: x in [:A,A:] \/ [:(X \ A),X:]

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: verum

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: verum