reconsider u = v as Term of the carrier of K345(S,V), by Th4;
the_sort_of v,A = the Sorts of A . (the_sort_of u) by Def2;
hence not the_sort_of v,A is empty ; :: thesis: verum