let G be _Graph; :: thesis: card (VertexDomRel G) c= G .size()
set E = the RepDEdgeSelection of G;
card the RepDEdgeSelection of G c= card (the_Edges_of G) by CARD_1:11;
then card the RepDEdgeSelection of G c= G .size() by GLIB_000:def 25;
then card (Class (DEdgeAdjEqRel G)) c= G .size() by GLIBPRE0:69;
hence card (VertexDomRel G) c= G .size() by Th10; :: thesis: verum