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 Vertex of G holds
( [v,w] in E iff v,w are_adjacent )
let E be symmetric Relation of V; :: thesis: for G being GraphFromSymRel of V,E
for v, w being Vertex of G holds
( [v,w] in E iff v,w are_adjacent )
let G be GraphFromSymRel of V,E; :: thesis: for v, w being Vertex of G holds
( [v,w] in E iff v,w are_adjacent )
let v, w be Vertex of G; :: thesis: ( [v,w] in E iff v,w are_adjacent )

hereby :: thesis: ( v,w are_adjacent implies [v,w] in E )

assume [v,w] in E ; :: thesis: v,w are_adjacent

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

suppose [v,w] DJoins v,w,G ; :: thesis: v,w are_adjacent

then [v,w] Joins v,w,G by GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

suppose [w,v] DJoins w,v,G ; :: thesis: v,w are_adjacent

then [w,v] Joins v,w,G by GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

end;

end;

set G0 = createGraph (V,E);
consider E0 being RepEdgeSelection of createGraph (V,E) such that
A1: G is inducedSubgraph of createGraph (V,E), the_Vertices_of (createGraph (V,E)),E0 by GLIB_009:def 7;
A2: 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 A3: the_Edges_of G = E0 by A1, A2, GLIB_000:def 37;
assume v,w are_adjacent ; :: thesis: [v,w] in E
then consider e being object such that
A4: e Joins v,w,G by CHORD:def 3;
e in E0 by A3, A4, GLIB_000:def 13;
then e in the_Edges_of (createGraph (V,E)) ;
then A5: e in E ;
then consider v0, w0 being object such that
A6: e = [v0,w0] by RELAT_1:def 1;
e DJoins v0,w0, createGraph (V,E) by A5, A6, Th63;
then A7: e Joins v0,w0, createGraph (V,E) by GLIB_000:16;
e Joins v,w, createGraph (V,E) by A4, GLIB_000:72;

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

suppose ( v = v0 & w = w0 ) ; :: thesis: [v,w] in E

hence [v,w] in E by A5, A6; :: thesis: verum

end;

suppose ( v = w0 & w = v0 ) ; :: thesis: [v,w] in E

hence [v,w] in E by A5, A6, GLIBPRE0:13; :: thesis: verum

end;

end;