let v be Vertex of G; :: thesis: ( v is isolated implies not v is cut-vertex )
assume A1: v is isolated ; :: thesis: not v is cut-vertex
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: not G .numComponents() in the removeVertex of G,v .numComponents()

per cases ( not G is _trivial or G is _trivial ) ;

suppose not G is _trivial ; :: thesis: not G .numComponents() in the removeVertex of G,v .numComponents()

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: verum

end;

suppose G is _trivial ; :: thesis: not G .numComponents() in the removeVertex of G,v .numComponents()

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: verum

end;

end;

end;

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