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

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

B1 * B2 c= [:X,X:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B1 * B2 or x in [:X,X:] )
assume A0: x in B1 * B2 ; :: thesis: x in [:X,X:]
then consider a, b being object such that
A1: x = [a,b] by RELAT_1:def 1;
consider c being object such that
A2: ( [a,c] in B1 & [c,b] in B2 ) by A0, A1, RELAT_1:def 8;
( B1 in cB & B2 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 ( B1 = {} & B2 = {} ) by SUBSET_1:def 1;
then B1 * B2 = {} ;
hence [*] is Subset of [:X,X:] by XBOOLE_1:2; :: thesis: verum

end;

end;