let V be non empty set ; :: thesis: for E being Relation of V holds VertexDomRel (createGraph (V,E)) = E
let E be Relation of V; :: thesis: VertexDomRel (createGraph (V,E)) = E
set G0 = createGraph (V,E);

now :: thesis: for v, w being object holds
( ( [v,w] in VertexDomRel (createGraph (V,E)) implies [v,w] in E ) & ( [v,w] in E implies [v,w] in VertexDomRel (createGraph (V,E)) ) )

let v, w be object ; :: thesis: ( ( [v,w] in VertexDomRel (createGraph (V,E)) implies [v,w] in E ) & ( [v,w] in E implies [v,w] in VertexDomRel (createGraph (V,E)) ) )

hereby :: thesis: ( [v,w] in E implies [v,w] in VertexDomRel (createGraph (V,E)) )

assume [v,w] in VertexDomRel (createGraph (V,E)) ; :: thesis: [v,w] in E
then consider e being object such that
A1: e DJoins v,w, createGraph (V,E) by Th1;
e in the_Edges_of (createGraph (V,E)) by A1, GLIB_000:def 14;
then A2: e in E ;
then consider v0, w0 being object such that
A3: e = [v0,w0] by RELAT_1:def 1;
e DJoins v0,w0, createGraph (V,E) by A2, A3, Th63;
then ( v0 = v & w0 = w ) by A1, GLIB_000:125;
hence [v,w] in E by A2, A3; :: thesis: verum

end;

assume [v,w] in E ; :: thesis: [v,w] in VertexDomRel (createGraph (V,E))
then [v,w] DJoins v,w, createGraph (V,E) by Th63;
hence [v,w] in VertexDomRel (createGraph (V,E)) by Th1; :: thesis: verum

end;

hence VertexDomRel (createGraph (V,E)) = E by RELAT_1:def 2; :: thesis: verum