theorem Th41: :: GLUNIR00:41

for G being _Graph holds card (Class (DEdgeAdjEqRel G)) c= card (VertexAdjSymRel G)