let G be non-Dmulti _Graph; :: thesis: G .size() = card (VertexDomRel G)
DEdgeAdjEqRel G = id (the_Edges_of G) by GLIB_009:71;
then Class (DEdgeAdjEqRel G) = SmallestPartition (the_Edges_of G) by EQREL_1:def 5;
then card (Class (DEdgeAdjEqRel G)) = card (the_Edges_of G) by TOPGEN_2:12;
then card (VertexDomRel G) = card (the_Edges_of G) by Th10;
hence G .size() = card (VertexDomRel G) by GLIB_000:def 25; :: thesis: verum