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 )
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;