theorem :: GLIBPRE1:61

for G1 being non _trivial connected _Graph
for G2 being non spanning Subgraph of G1 ex v, e, w being object st
( v <> w & e DJoins v,w,G1 & not e in the_Edges_of G2 & ( for G3 being addAdjVertex of G2,v,e,w holds G3 is Subgraph of G1 ) & ( ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 ) or ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ) )