for G being _Graph
for G0 being Subgraph of G
for S being non empty Subset of (the_Vertices_of G)
for x being Vertex of G
for G1 being inducedSubgraph of G,S
for G2 being inducedSubgraph of G,(S \/ {x}) st G1 is connected & x in G .AdjacentSet (the_Vertices_of G1) holds
G2 is connected