card the carrier of K in NAT ;
hence card K is Element of NAT ; :: thesis: verum