let G be connected _Graph; :: thesis: for v being Vertex of holds
( not v is cut-vertex iff for G2 being removeVertex of (the_Vertices_of G), holds G2 .numComponents() c= G .numComponents() )
let v be Vertex of ; :: thesis: ( not v is cut-vertex iff for G2 being removeVertex of (the_Vertices_of G), holds G2 .numComponents() c= G .numComponents() )

hereby :: thesis: ( ( for G2 being removeVertex of (the_Vertices_of G), holds G2 .numComponents() c= G .numComponents() ) implies not v is cut-vertex )

assume not v is cut-vertex ; :: thesis: for G2 being removeVertex of (the_Vertices_of G), holds G2 .numComponents() c= G .numComponents()
then consider G3 being removeVertex of (the_Vertices_of G), such that
A1: not G .numComponents() in G3 .numComponents() by Def10;
let G2 be removeVertex of (the_Vertices_of G),; :: thesis: G2 .numComponents() c= G .numComponents()
G3 .numComponents() c= G .numComponents() by A1, CARD_1:14;
hence G2 .numComponents() c= G .numComponents() by Lm12, GLIB_000:96; :: thesis: verum

end;

assume A2: for G2 being removeVertex of (the_Vertices_of G), holds G2 .numComponents() c= G .numComponents() ; :: thesis: not v is cut-vertex

now

consider X being removeVertex of (the_Vertices_of G),;
assume for G3 being removeVertex of (the_Vertices_of G), holds G .numComponents() in G3 .numComponents() ; :: thesis: contradiction
then A3: G .numComponents() in X .numComponents() ;
X .numComponents() c= G .numComponents() by A2;
hence contradiction by A3, CARD_1:14; :: thesis: verum

end;

hence not v is cut-vertex by Def10; :: thesis: verum