let G be non _trivial _Graph; :: thesis: for v being Vertex of G
for H being removeVertex of G,v holds VertexDomRel H = (VertexDomRel 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 VertexDomRel H = (VertexDomRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:])
let H be removeVertex of G,v; :: thesis: VertexDomRel H = (VertexDomRel 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 c= {v} by XBOOLE_1:37;
hence VertexDomRel H = (VertexDomRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:]) by Th22, XBOOLE_0:def 8; :: thesis: verum