let G be non _trivial _Graph; :: thesis: for v being Vertex of G
for H being removeVertex of G,v st v is isolated holds
VertexAdjSymRel H = VertexAdjSymRel G
let v be Vertex of G; :: thesis: for H being removeVertex of G,v st v is isolated holds
VertexAdjSymRel H = VertexAdjSymRel G
let H be removeVertex of G,v; :: thesis: ( v is isolated implies VertexAdjSymRel H = VertexAdjSymRel G )
assume v is isolated ; :: thesis: VertexAdjSymRel H = VertexAdjSymRel G
then VertexDomRel H = VertexDomRel G by Th24;
hence VertexAdjSymRel H = VertexAdjSymRel G ; :: thesis: verum