Het f <> 0 by HetHomo;
hence not HetSet f is empty ; :: thesis: verum