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;