the Element of A * the Element of B in A ** B by Th89;
hence not A ** B is empty ; :: thesis: verum