per cases ( not cB is empty or cB is empty ) ;

suppose A3: not cB is empty ; :: thesis: [~] is Subset of [:X,X:]

B ~ c= [:X,X:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B ~ or x in [:X,X:] )
assume A0: x in B ~ ; :: thesis: x in [:X,X:]
then consider a, b being object such that
A1: x = [a,b] by RELAT_1:def 1;
A2: [b,a] in B by A0, A1, RELAT_1:def 7;
B in cB by A3;
then ( b in X & a in X ) by A2, ZFMISC_1:87;
hence x in [:X,X:] by A1, ZFMISC_1:87; :: thesis: verum

end;

hence [~] is Subset of [:X,X:] ; :: thesis: verum

end;

suppose cB is empty ; :: thesis: [~] is Subset of [:X,X:]

then B = {} by SUBSET_1:def 1;
then B ~ = {} ;
hence [~] is Subset of [:X,X:] by XBOOLE_1:2; :: thesis: verum

end;

end;