let V be non empty set ; :: thesis: for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v, w being object holds
( [v,w] in E iff ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) )
let E be symmetric Relation of V; :: thesis: for G being GraphFromSymRel of V,E
for v, w being object holds
( [v,w] in E iff ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) )
let G be GraphFromSymRel of V,E; :: thesis: for v, w being object holds
( [v,w] in E iff ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) )
let v, w be object ; :: thesis: ( [v,w] in E iff ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) )
A1: ( v is set & w is set ) by TARSKI:1;
set G0 = createGraph (V,E);
consider E0 being RepEdgeSelection of createGraph (V,E) such that
A2: G is inducedSubgraph of createGraph (V,E), the_Vertices_of (createGraph (V,E)),E0 by GLIB_009:def 7;

hereby :: thesis: ( ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) implies [v,w] in E )

assume [v,w] in E ; :: thesis: ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G )
then A3: ( [v,w] DJoins v,w, createGraph (V,E) & [w,v] DJoins w,v, createGraph (V,E) ) by Th63, GLIBPRE0:13;
[v,w] Joins v,w, createGraph (V,E) by A3, GLIB_000:16;
then consider e being object such that
A4: ( e Joins v,w, createGraph (V,E) & e in E0 ) and
for e9 being object st e9 Joins v,w, createGraph (V,E) & e9 in E0 holds
e9 = e by GLIB_009:def 5;
e in the_Edges_of (createGraph (V,E)) by A4;
then A5: e in E ;
then consider v0, w0 being object such that
A6: e = [v0,w0] by RELAT_1:def 1;
A7: e DJoins v0,w0, createGraph (V,E) by A5, A6, Th63;
A8: the_Edges_of (createGraph (V,E)) = (createGraph (V,E)) .edgesBetween (the_Vertices_of (createGraph (V,E))) by GLIB_000:34;
the_Vertices_of (createGraph (V,E)) c= the_Vertices_of (createGraph (V,E)) ;
then A9: E0 = the_Edges_of G by A2, A8, GLIB_000:def 37;
( e is set & v0 is set & w0 is set ) by TARSKI:1;
then A10: e DJoins v0,w0,G by A4, A7, A9, GLIB_000:73;
e Joins v0,w0, createGraph (V,E) by A7, GLIB_000:16;

per cases then ( ( v = v0 & w = w0 ) or ( v = w0 & w = v0 ) ) by A4, GLIB_000:15;

suppose ( v = v0 & w = w0 ) ; :: thesis: ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G )

hence ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) by A6, A10; :: thesis: verum

end;

suppose ( v = w0 & w = v0 ) ; :: thesis: ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G )

hence ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) by A6, A10; :: thesis: verum

end;

end;

end;

assume ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) ; :: thesis: [v,w] in E

per cases then ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) ;

suppose [v,w] DJoins v,w,G ; :: thesis: [v,w] in E

hence [v,w] in E by A1, Th63, GLIB_000:72; :: thesis: verum

end;

suppose [w,v] DJoins w,v,G ; :: thesis: [v,w] in E

then [w,v] DJoins w,v, createGraph (V,E) by A1, GLIB_000:72;
hence [v,w] in E by Th63, GLIBPRE0:13; :: thesis: verum

end;

end;