theorem :: GLIB_009:69

for G being _Graph holds DEdgeAdjEqRel G c= EdgeAdjEqRel G