let G be connected _Graph; :: thesis: for v being Vertex of G holds
( not v is cut-vertex iff for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() )
let v be Vertex of G; :: thesis: ( not v is cut-vertex iff for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() )
hereby :: thesis: ( ( for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() ) implies not v is cut-vertex )
assume not v is cut-vertex ; :: thesis: for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents()
then consider G3 being removeVertex of G,v such that
A1: not G .numComponents() in G3 .numComponents() ;
let G2 be removeVertex of G,v; :: thesis: G2 .numComponents() c= G .numComponents()
G3 .numComponents() c= G .numComponents() by A1, CARD_1:4;
hence G2 .numComponents() c= G .numComponents() by Lm12, GLIB_000:93; :: thesis: verum
end;
assume A2: for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() ; :: thesis: not v is cut-vertex
now :: thesis: not for G3 being removeVertex of G,v holds G .numComponents() in G3 .numComponents()
set X = the removeVertex of G,v;
assume for G3 being removeVertex of G,v holds G .numComponents() in G3 .numComponents() ; :: thesis: contradiction
then A3: G .numComponents() in the removeVertex of G,v .numComponents() ;
the removeVertex of G,v .numComponents() c= G .numComponents() by A2;
hence contradiction by A3, CARD_1:4; :: thesis: verum
end;
hence not v is cut-vertex ; :: thesis: verum