now :: thesis: for i being object st i in the carrier of S holds
not (Constants U0) . i is empty

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

end;

hence Constants U0 is non-empty ; :: thesis: verum