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