let G be connected _Graph; :: thesis: for v being Vertex of G
for G2 being removeVertex of G,v st not v is cut-vertex holds
G2 is connected
let v be Vertex of G; :: thesis: for G2 being removeVertex of G,v st not v is cut-vertex holds
G2 is connected
let G2 be removeVertex of G,v; :: thesis: ( not v is cut-vertex implies G2 is connected )
assume A1: not v is cut-vertex ; :: thesis: G2 is connected
G .numComponents() = 1 by Lm18;
then G2 .numComponents() c= succ 0 by A1, Lm19;
then G2 .numComponents() c= {} \/ {{}} ;
then G2 .numComponents() = {} \/ {{}} by ZFMISC_1:33
.= succ 0
.= 1 ;
hence G2 is connected by Lm18; :: thesis: verum