let G be _Graph; :: thesis: for H being removeLoops of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))
let H be removeLoops of G; :: thesis: VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))
A1: VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G)) by Th17;
then (VertexDomRel H) ~ = ((VertexDomRel G) ~) \ ((id (the_Vertices_of G)) ~) by RELAT_1:24
.= ((VertexDomRel G) ~) \ (id (the_Vertices_of G)) ;
hence VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G)) by A1, XBOOLE_1:42; :: thesis: verum