let D be set ; :: thesis: ( D is HP-closed implies not D is empty )
assume D is HP-closed ; :: thesis: not D is empty
then D is with_VERUM ;
hence not D is empty ; :: thesis: verum