let G2 be _Graph; for v1 being set
for e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
G2 is removeVertex of G1,v1
let v1 be set ; for e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
G2 is removeVertex of G1,v1
let e be object ; for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
G2 is removeVertex of G1,v1
let v2 be Vertex of G2; for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
G2 is removeVertex of G1,v1
let G1 be addAdjVertex of G2,v1,e,v2; ( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 implies G2 is removeVertex of G1,v1 )
assume A1:
( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 )
; G2 is removeVertex of G1,v1
then
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v1}
by Def14;
then
the_Vertices_of G2 = (the_Vertices_of G1) \ {v1}
by A1, ZFMISC_1:117;
hence
G2 is removeVertex of G1,v1
by Th140; verum