let G2 be _Graph; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum