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

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