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 G' = G as trivial _Graph ;
A2: G' .numComponents() = 1 by Lm18;
consider G2 being removeVertex of G',v;
G2 .numComponents() = 1 by Lm18;
then 1 in 1 by A1, A2, Def10;
hence contradiction ; :: thesis: verum

end;

hence not G is trivial ; :: thesis: verum