consider s being SortSymbol of S;
reconsider St = the Sorts of U1 as V2 ManySortedSet of the carrier of S ;
dom the Sorts of U1 = the carrier of S by PBOOLE:def 3;
then A1: the Sorts of U1 . s in rng the Sorts of U1 by FUNCT_1:def 5;
consider x being set such that
A2: x in St . s by XBOOLE_0:def 1;
thus not |.U1.| is empty by A1, A2, TARSKI:def 4; :: thesis: verum