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

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, Def10;
hence contradiction ; :: thesis: verum

end;

hence not G is trivial ; :: thesis: verum