let G2 be _Graph; for v being object
for V being non empty set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G1 <> {}
let v be object ; for V being non empty set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G1 <> {}
let V be non empty set ; for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G1 <> {}
let G1 be addAdjVertexAll of G2,v,V; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies the_Edges_of G1 <> {} )
assume
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
; the_Edges_of G1 <> {}
then consider E being set such that
A1:
( card V = card E & E misses the_Edges_of G2 )
and
A2:
the_Edges_of G1 = (the_Edges_of G2) \/ E
and
for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) )
by Def4;
not E is empty
by A1;
then consider e being object such that
A3:
e in E
by XBOOLE_0:def 1;
thus
the_Edges_of G1 <> {}
by A2, A3; verum