take NAT ; :: thesis: ( not NAT is empty & NAT is ordinal )
thus ( not NAT is empty & NAT is ordinal ) ; :: thesis: verum