let G be _Graph; for H being removeParallelEdges of G holds VertexAdjSymRel H = VertexAdjSymRel G
let H be removeParallelEdges of G; 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 for v, w being object st [v,w] in VertexAdjSymRel G holds
[v,w] in VertexAdjSymRel Hlet v,
w be
object ;
( [v,w] in VertexAdjSymRel G implies [v,w] in VertexAdjSymRel H )assume
[v,w] in VertexAdjSymRel G
;
[v,w] in VertexAdjSymRel Hthen 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;
verum end;
then
VertexAdjSymRel G c= VertexAdjSymRel H
by RELAT_1:def 3;
hence
VertexAdjSymRel H = VertexAdjSymRel G
by A2, XBOOLE_0:def 10; verum