now :: thesis: for i being object st i in the carrier of S holds

not (Constants U0) . i is empty

hence
Constants U0 is non-empty
; :: thesis: verumnot (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;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