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