let V be non empty set ; :: thesis: for E being Relation of V
for v, w being object holds
( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )
let E be Relation of V; :: thesis: for v, w being object holds
( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )
let v, w be object ; :: thesis: ( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )
set G0 = createGraph (V,E);

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

assume A1: [v,w] in E ; :: thesis: [v,w] DJoins v,w, createGraph (V,E)
then A2: [v,w] in the_Edges_of (createGraph (V,E)) ;
A3: ( v in V & w in V ) by A1, ZFMISC_1:87;
A4: (the_Source_of (createGraph (V,E))) . [v,w] = ((pr1 (V,V)) | E) . [v,w]
.= (pr1 (V,V)) . [v,w] by A1, FUNCT_1:49
.= (pr1 (V,V)) . (v,w) by BINOP_1:def 1
.= v by A3, FUNCT_3:def 4 ;
(the_Target_of (createGraph (V,E))) . [v,w] = ((pr2 (V,V)) | E) . [v,w]
.= (pr2 (V,V)) . [v,w] by A1, FUNCT_1:49
.= (pr2 (V,V)) . (v,w) by BINOP_1:def 1
.= w by A3, FUNCT_3:def 5 ;
hence [v,w] DJoins v,w, createGraph (V,E) by A2, A4, GLIB_000:def 14; :: thesis: verum

end;

assume [v,w] DJoins v,w, createGraph (V,E) ; :: thesis: [v,w] in E
then [v,w] in the_Edges_of (createGraph (V,E)) by GLIB_000:def 14;
hence [v,w] in E ; :: thesis: verum