let G be _Graph; :: thesis: for H being removeParallelEdges of G holds VertexAdjSymRel H = VertexAdjSymRel G
let H be removeParallelEdges of G; :: thesis: VertexAdjSymRel H = VertexAdjSymRel G
consider E being RepEdgeSelection of G such that
A1: H is inducedSubgraph of G, the_Vertices_of G,E by GLIB_009:def 7;
A2: VertexAdjSymRel H c= VertexAdjSymRel G by Th45;

now :: thesis: for v, w being object st [v,w] in VertexAdjSymRel G holds
[v,w] in VertexAdjSymRel H

let v, w be object ; :: thesis: ( [v,w] in VertexAdjSymRel G implies [v,w] in VertexAdjSymRel H )
assume [v,w] in VertexAdjSymRel G ; :: thesis: [v,w] in VertexAdjSymRel H
then consider e0 being object such that
A3: e0 Joins v,w,G by Th32;
( the_Edges_of G = G .edgesBetween (the_Vertices_of G) & the_Vertices_of G c= the_Vertices_of G ) by GLIB_000:34;
then A4: the_Edges_of H = E by A1, GLIB_000:def 37;
consider e being object such that
A5: ( e Joins v,w,G & e in E ) and
for e9 being object st e9 Joins v,w,G & e9 in E holds
e9 = e by A3, GLIB_009:def 5;
( v is set & w is set ) by TARSKI:1;
then e Joins v,w,H by A4, A5, GLIB_000:73;
hence [v,w] in VertexAdjSymRel H by Th32; :: thesis: verum

end;

then VertexAdjSymRel G c= VertexAdjSymRel H by RELAT_1:def 3;
hence VertexAdjSymRel H = VertexAdjSymRel G by A2, XBOOLE_0:def 10; :: thesis: verum