let G be _Graph; :: thesis: for v being Vertex of G st v is cut-vertex holds

not G is trivial

let v be Vertex of G; :: thesis: ( v is cut-vertex implies not G is trivial )

assume A1: v is cut-vertex ; :: thesis: not G is trivial

not G is trivial

let v be Vertex of G; :: thesis: ( v is cut-vertex implies not G is trivial )

assume A1: v is cut-vertex ; :: thesis: not G is trivial

now :: thesis: not G is trivial

hence
not G is trivial
; :: thesis: verumassume
G is trivial
; :: thesis: contradiction

then reconsider G9 = G as trivial _Graph ;

set G2 = the removeVertex of G9,v;

( G9 .numComponents() = 1 & the removeVertex of G9,v .numComponents() = 1 ) by Lm18;

then 1 in 1 by A1;

hence contradiction ; :: thesis: verum

end;then reconsider G9 = G as trivial _Graph ;

set G2 = the removeVertex of G9,v;

( G9 .numComponents() = 1 & the removeVertex of G9,v .numComponents() = 1 ) by Lm18;

then 1 in 1 by A1;

hence contradiction ; :: thesis: verum