let G be _Graph; :: thesis: card (Class (DEdgeAdjEqRel G)) c= card (VertexAdjSymRel G)
card (VertexDomRel G) c= card (VertexAdjSymRel G) by Th34, CARD_1:11;
hence card (Class (DEdgeAdjEqRel G)) c= card (VertexAdjSymRel G) by Th10; :: thesis: verum