let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies VertexDomRel G1 = VertexDomRel G2 )
assume A1: G1 == G2 ; :: thesis: VertexDomRel G1 = VertexDomRel G2

now :: thesis: for v, w being object holds
( ( [v,w] in VertexDomRel G1 implies [v,w] in VertexDomRel G2 ) & ( [v,w] in VertexDomRel G2 implies [v,w] in VertexDomRel G1 ) )

let v, w be object ; :: thesis: ( ( [v,w] in VertexDomRel G1 implies [v,w] in VertexDomRel G2 ) & ( [v,w] in VertexDomRel G2 implies [v,w] in VertexDomRel G1 ) )

hereby :: thesis: ( [v,w] in VertexDomRel G2 implies [v,w] in VertexDomRel G1 )

assume [v,w] in VertexDomRel G1 ; :: thesis: [v,w] in VertexDomRel G2
then consider e being object such that
A2: e DJoins v,w,G1 by Th1;
e DJoins v,w,G2 by A1, A2, GLIB_000:88;
hence [v,w] in VertexDomRel G2 by Th1; :: thesis: verum

end;

assume [v,w] in VertexDomRel G2 ; :: thesis: [v,w] in VertexDomRel G1
then consider e being object such that
A3: e DJoins v,w,G2 by Th1;
e DJoins v,w,G1 by A1, A3, GLIB_000:88;
hence [v,w] in VertexDomRel G1 by Th1; :: thesis: verum

end;

hence VertexDomRel G1 = VertexDomRel G2 by RELAT_1:def 2; :: thesis: verum