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