set a1 = the Element of C1;
set a2 = the Element of C2;
[: the Element of C1, the Element of C2:] in C1 [*] C2 by Th96;
hence not C1 [*] C2 is empty ; :: thesis: verum