theorem :: GLIB_002:37
for G being finite non trivial connected _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) by Lm21;