let G be _Graph; :: thesis: ( card (G .degreeMap()) = G .order() & card (G .inDegreeMap()) = G .order() & card (G .outDegreeMap()) = G .order() )
( dom (G .degreeMap()) = the_Vertices_of G & dom (G .inDegreeMap()) = the_Vertices_of G & dom (G .outDegreeMap()) = the_Vertices_of G ) by PARTFUN1:def 2;
hence ( card (G .degreeMap()) = G .order() & card (G .inDegreeMap()) = G .order() & card (G .outDegreeMap()) = G .order() ) by CARD_1:62; :: thesis: verum