v .inDegree() = card (v .edgesIn()) ;
hence v .inDegree() is Element of NAT ; :: thesis: verum