reconsider u = v as Term of 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