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