let X be set ; :: thesis: for A being Subset of X holds [:A,A:] \/ [:(X \ A),(X \ A):] c= [:(X \ A),X:] \/ [:X,A:]
let A be Subset of X; :: thesis: [:A,A:] \/ [:(X \ A),(X \ A):] c= [:(X \ A),X:] \/ [:X,A:]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:A,A:] \/ [:(X \ A),(X \ A):] or x in [:(X \ A),X:] \/ [:X,A:] )
assume x in [:A,A:] \/ [:(X \ A),(X \ A):] ; :: thesis: x in [:(X \ A),X:] \/ [:X,A:]

per cases then ( x in [:A,A:] or x in [:(X \ A),(X \ A):] ) by XBOOLE_0:def 3;

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

then consider y, z being object such that
A1: y in A and
A2: z in A and
A3: x = [y,z] by ZFMISC_1:def 2;
( x in [:(X \ A),X:] or x in [:X,A:] ) by A1, A2, A3, ZFMISC_1:87;
hence x in [:(X \ A),X:] \/ [:X,A:] by XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider y, z being object such that
A4: y in X \ A and
A5: z in X \ A and
A6: x = [y,z] by ZFMISC_1:def 2;
( x in [:(X \ A),X:] or x in [:X,A:] ) by A4, A5, A6, ZFMISC_1:87;
hence x in [:(X \ A),X:] \/ [:X,A:] by XBOOLE_0:def 3; :: thesis: verum

end;

end;