reconsider u = v as Term of the carrier of K345(S,V), by Th4;
take the Sorts of A . (the_sort_of u) ; :: thesis: for u being Term of the carrier of K345(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 the carrier of K345(S,V), st u = v holds
the Sorts of A . (the_sort_of u) = the Sorts of A . (the_sort_of u) ; :: thesis: verum