take NAT ; :: thesis: ( NAT is infinite & NAT is natural-membered )
thus ( NAT is infinite & NAT is natural-membered ) ; :: thesis: verum