for G1 being non _trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is isolated holds
( G1 .componentSet() = (G2 .componentSet()) \/ {{v}} & G1 .numComponents() = (G2 .numComponents()) +` 1 )