let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st the_Vertices_of G3 misses V holds
not G1 is connected
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st the_Vertices_of G3 misses V holds
not G1 is connected
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st the_Vertices_of G3 misses V holds
not G1 is connected
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st the_Vertices_of G3 misses V implies not G1 is connected )
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ex G3 being Component of G2 st the_Vertices_of G3 misses V ; :: thesis: not G1 is connected
ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V

proof

consider G3 being Component of G2 such that
A3: the_Vertices_of G3 misses V by A2;
take G3 ; :: thesis: for w being Vertex of G3 holds not w in V
let w be Vertex of G3; :: thesis: not w in V
(the_Vertices_of G3) /\ V = {} by A3, XBOOLE_0:def 7;
hence not w in V by Lm7; :: thesis: verum

end;

hence not G1 is connected by A1, Th73; :: thesis: verum