let G2 be _Graph; :: thesis: for v being object
for V being set
for W being Subset of V
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G1 .edgesBetween (W,{v}) = {} holds
W = {}
let v be object ; :: thesis: for V being set
for W being Subset of V
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G1 .edgesBetween (W,{v}) = {} holds
W = {}
let V be set ; :: thesis: for W being Subset of V
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G1 .edgesBetween (W,{v}) = {} holds
W = {}
let W be Subset of V; :: thesis: for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G1 .edgesBetween (W,{v}) = {} holds
W = {}
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G1 .edgesBetween (W,{v}) = {} implies W = {} )
assume ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: ( not G1 .edgesBetween (W,{v}) = {} or W = {} )
then consider E being set such that
card V = card E and
( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A1: 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;
assume A2: G1 .edgesBetween (W,{v}) = {} ; :: thesis: W = {}
assume A3: W <> {} ; :: thesis: contradiction
set w = the Element of W;
the Element of W in W by A3;
then consider e being object such that
A4: ( e in E & e Joins the Element of W,v,G1 ) and
for e2 being object st e2 Joins the Element of W,v,G1 holds
e = e2 by A1;
v in {v} by TARSKI:def 1;
then e SJoins W,{v},G1 by A3, A4, GLIB_000:17;
hence contradiction by A2, GLIB_000:def 30; :: thesis: verum