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