now

let i be set ; :: 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 Def5;
hence not (Constants U0) . i is empty ; :: thesis: verum

end;

hence Constants U0 is non-empty by PBOOLE:def 16; :: thesis: verum