reconsider u = v as Term of S,V by Th4;
take the Sorts of A . (the_sort_of u) ; :: thesis: for u being Term of S,V st u = v holds
the Sorts of A . (the_sort_of u) = the Sorts of A . (the_sort_of u)
thus for u being Term of S,V st u = v holds
the Sorts of A . (the_sort_of u) = the Sorts of A . (the_sort_of u) ; :: thesis: verum