let X be set ; :: thesis: for A being Subset of X holds [:(X \ A),X:] \/ [:X,A:] c= [:X,X:]
let A be Subset of X; :: thesis: [:(X \ A),X:] \/ [:X,A:] c= [:X,X:]
( [:X,A:] c= [:X,X:] & [:(X \ A),X:] c= [:X,X:] ) by ZFMISC_1:95;
hence [:(X \ A),X:] \/ [:X,A:] c= [:X,X:] by XBOOLE_1:8; :: thesis: verum