take NAT ; :: thesis: ( not NAT is empty & NAT is add-closed & NAT is natural-membered )
thus ( not NAT is empty & NAT is add-closed & NAT is natural-membered ) ; :: thesis: verum