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