let G be non _trivial _Graph; for v1, e being object
for v2 being Vertex of G
for G1 being addAdjVertex of G,v1,e,v2
for G2 being removeVertex of G1,v2
for G3 being removeVertex of G,v2 st not e in the_Edges_of G & not v1 in the_Vertices_of G holds
G2 is addVertex of G3,v1
let v1, e be object ; for v2 being Vertex of G
for G1 being addAdjVertex of G,v1,e,v2
for G2 being removeVertex of G1,v2
for G3 being removeVertex of G,v2 st not e in the_Edges_of G & not v1 in the_Vertices_of G holds
G2 is addVertex of G3,v1
let v2 be Vertex of G; for G1 being addAdjVertex of G,v1,e,v2
for G2 being removeVertex of G1,v2
for G3 being removeVertex of G,v2 st not e in the_Edges_of G & not v1 in the_Vertices_of G holds
G2 is addVertex of G3,v1
let G1 be addAdjVertex of G,v1,e,v2; for G2 being removeVertex of G1,v2
for G3 being removeVertex of G,v2 st not e in the_Edges_of G & not v1 in the_Vertices_of G holds
G2 is addVertex of G3,v1
let G2 be removeVertex of G1,v2; for G3 being removeVertex of G,v2 st not e in the_Edges_of G & not v1 in the_Vertices_of G holds
G2 is addVertex of G3,v1
let G3 be removeVertex of G,v2; ( not e in the_Edges_of G & not v1 in the_Vertices_of G implies G2 is addVertex of G3,v1 )
assume A1:
( not e in the_Edges_of G & not v1 in the_Vertices_of G )
; G2 is addVertex of G3,v1
A2:
( v2 is Vertex of G1 & v1 <> v2 )
by A1, Th72;
A3: the_Vertices_of G2 =
(the_Vertices_of G1) \ {v2}
by A2, GLIB_000:47
.=
((the_Vertices_of G) \/ {v1}) \ {v2}
by A1, Def12
.=
((the_Vertices_of G) \ {v2}) \/ ({v1} \ {v2})
by XBOOLE_1:42
.=
((the_Vertices_of G) \ {v2}) \/ {v1}
by A2, ZFMISC_1:14
.=
(the_Vertices_of G3) \/ {v1}
by GLIB_000:47
;
for e1 being object holds
( e1 in G1 .edgesBetween ((the_Vertices_of G1) \ {v2}) iff e1 in G .edgesBetween ((the_Vertices_of G) \ {v2}) )
then A13:
G1 .edgesBetween ((the_Vertices_of G1) \ {v2}) = G .edgesBetween ((the_Vertices_of G) \ {v2})
by TARSKI:2;
A14: the_Edges_of G2 =
G1 .edgesBetween ((the_Vertices_of G1) \ {v2})
by A2, GLIB_000:47
.=
the_Edges_of G3
by A13, GLIB_000:47
;
( dom (the_Source_of G2) = the_Edges_of G2 & dom (the_Target_of G2) = the_Edges_of G2 )
by GLIB_000:4;
then A16:
( dom (the_Source_of G2) = dom (the_Source_of G3) & dom (the_Target_of G2) = dom (the_Target_of G3) )
by A14, GLIB_000:4;
for e1 being object st e1 in dom (the_Source_of G2) holds
(the_Source_of G2) . e1 = (the_Source_of G3) . e1
then A19:
the_Source_of G2 = the_Source_of G3
by A16, FUNCT_1:2;
for e1 being object st e1 in dom (the_Target_of G2) holds
(the_Target_of G2) . e1 = (the_Target_of G3) . e1
then A22:
the_Target_of G2 = the_Target_of G3
by A16, FUNCT_1:2;
then
G2 is Supergraph of G3
by Def9;
hence
G2 is addVertex of G3,v1
by A3, A14, A19, A22, Def10; verum