let G2 be _Graph; 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 ; 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 ; 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; 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; ( 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 )
; ( 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}) = {}
; W = {}
assume A3:
W <> {}
; 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; verum