let X be set ; for A being Subset of X holds [:(X \ A),X:] \/ [:X,A:] = [:A,A:] \/ [:(X \ A),X:]
let A be Subset of X; [:(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 ;
TARSKI:def 3 ( 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:]
;
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
;
x in [:A,A:] \/ [:(X \ A),X:]
x in [:X,A:]
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;
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; verum