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