let V be non empty set ; :: thesis: for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds VertexAdjSymRel G = E
let E be symmetric Relation of V; :: thesis: for G being GraphFromSymRel of V,E holds VertexAdjSymRel G = E
let G be GraphFromSymRel of V,E; :: thesis: VertexAdjSymRel G = E

now :: thesis: for x, y being object holds
( ( [x,y] in VertexAdjSymRel G implies [x,y] in E ) & ( [x,y] in E implies [x,y] in VertexAdjSymRel G ) )

let x, y be object ; :: thesis: ( ( [x,y] in VertexAdjSymRel G implies [x,y] in E ) & ( [x,y] in E implies [x,y] in VertexAdjSymRel G ) )

hereby :: thesis: ( [x,y] in E implies [x,y] in VertexAdjSymRel G )

assume A1: [x,y] in VertexAdjSymRel G ; :: thesis: [x,y] in E
then reconsider v = x, w = y as Vertex of G by ZFMISC_1:87;
v,w are_adjacent by A1, Th33;
hence [x,y] in E by Th89; :: thesis: verum

end;

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;
A3: 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 A4: the_Vertices_of G = the_Vertices_of (createGraph (V,E)) by A2, A3, GLIB_000:def 37
.= V ;
assume A5: [x,y] in E ; :: thesis: [x,y] in VertexAdjSymRel G
then reconsider v = x, w = y as Vertex of G by A4, ZFMISC_1:87;
v,w are_adjacent by A5, Th89;
hence [x,y] in VertexAdjSymRel G by Th33; :: thesis: verum

end;

hence VertexAdjSymRel G = E by RELAT_1:def 2; :: thesis: verum