let v be Vertex of G; :: thesis:
assume A1: v is isolated ; :: thesis:
not for G2 being removeVertex of G,v holds G .numComponents() in G2 .numComponents()

proof

set G2 = the removeVertex of G,v;
take the removeVertex of G,v ; :: thesis:

per cases ;

suppose not G is _trivial ; :: thesis:

then G .numComponents() = ( the removeVertex of G,v .numComponents()) +` 1 by A1, Th57;
hence not G .numComponents() in the removeVertex of G,v .numComponents() by ORDINAL1:5, CARD_2:94; :: thesis:

end;

suppose G is _trivial ; :: thesis:

then consider v1 being Vertex of G such that
A2: the_Vertices_of G = {v1} by GLIB_000:22;
v = v1 by A2, TARSKI:def 1;
then (the_Vertices_of G) \ {v} is empty by A2, XBOOLE_1:37;
then G == the removeVertex of G,v by GLIB_000:def 37;
then G .numComponents() = the removeVertex of G,v .numComponents() by GLIB_002:29;
hence not G .numComponents() in the removeVertex of G,v .numComponents() ; :: thesis:

end;

end;

end;

hence not v is cut-vertex by GLIB_002:def 10; :: thesis: