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

assume A1: v is cut-vertex ; :: thesis: for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents()
let G2 be removeVertex of G,v; :: thesis: G .numComponents() < G2 .numComponents()
card (Segm (G .numComponents())) in card (Segm (G2 .numComponents())) by A1;
hence G .numComponents() < G2 .numComponents() by NAT_1:41; :: thesis: verum

end;

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

now :: thesis: for G2 being removeVertex of G,v holds G .numComponents() in G2 .numComponents()

let G2 be removeVertex of G,v; :: thesis: G .numComponents() in G2 .numComponents()
G .numComponents() < G2 .numComponents() by A2;
then card (Segm (G .numComponents())) in card (Segm (G2 .numComponents())) by NAT_1:41;
hence G .numComponents() in G2 .numComponents() ; :: thesis: verum

end;

hence v is cut-vertex ; :: thesis: verum