let G be non _trivial _Graph; :: thesis: for v being Vertex of G
for H being removeVertex of G,v holds VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:])
let v be Vertex of G; :: thesis: for H being removeVertex of G,v holds VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:])
let H be removeVertex of G,v; :: thesis: VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:])
not (the_Vertices_of G) \ {v} is empty by GLIB_000:20;
then not the_Vertices_of G = {v} by XBOOLE_1:37;
hence VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:]) by Th52, XBOOLE_0:def 8; :: thesis: verum