v .outDegree() = card (v .edgesOut()) ;
hence v .outDegree() is Element of NAT ; :: thesis: verum