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