take HP-WFF ; :: thesis: ( HP-WFF is HP-closed & not HP-WFF is empty )
thus ( HP-WFF is HP-closed & not HP-WFF is empty ) ; :: thesis: verum