let i be object ; :: thesis: ( i in the carrier of S implies not (Constants U0) . i is empty )
assume i in the carrier of S ; :: thesis: not (Constants U0) . i is empty
then reconsider s = i as SortSymbol of S ;
(Constants U0) . s = Constants (U0,s) by Def4;
hence not (Constants U0) . i is empty ; :: thesis: verum