ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) by Lm21;
hence not for b₁ being Vertex of G holds b₁ is cut-vertex ; :: thesis: verum