let G be _Graph; :: thesis: for H being SimpleGraph of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))
let H be SimpleGraph of G; :: thesis: VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))
consider G9 being removeParallelEdges of G such that
A1: H is removeLoops of G9 by GLIB_009:119;
A2: the_Vertices_of G9 = the_Vertices_of G by GLIB_000:def 33;
thus VertexAdjSymRel H = (VertexAdjSymRel G9) \ (id (the_Vertices_of G9)) by A1, Th47
.= (VertexAdjSymRel G) \ (id (the_Vertices_of G)) by A2, Th46 ; :: thesis: verum