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

now :: thesis: not G is _trivial

assume 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;

hence not G is _trivial ; :: thesis: verum