let G be non-Dmulti _Graph; :: thesis: G .size() c= card (VertexAdjSymRel G)
card (VertexDomRel G) = card (Class (DEdgeAdjEqRel G)) by Th10;
then G .size() = card (Class (DEdgeAdjEqRel G)) by Th12;
hence G .size() c= card (VertexAdjSymRel G) by Th41; :: thesis: verum