let G be _Graph; :: thesis: DEdgeAdjEqRel G c= EdgeAdjEqRel G

now :: thesis: for e1, e2 being object st [e1,e2] in DEdgeAdjEqRel G holds
[e1,e2] in EdgeAdjEqRel G

let e1, e2 be object ; :: thesis: ( [e1,e2] in DEdgeAdjEqRel G implies [e1,e2] in EdgeAdjEqRel G )
assume [e1,e2] in DEdgeAdjEqRel G ; :: thesis: [e1,e2] in EdgeAdjEqRel G
then consider v1, v2 being object such that
A1: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) by Def4;
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) by A1, GLIB_000:16;
hence [e1,e2] in EdgeAdjEqRel G by Def3; :: thesis: verum

end;

hence DEdgeAdjEqRel G c= EdgeAdjEqRel G by RELAT_1:def 3; :: thesis: verum