let G1 be non _trivial _Graph; for v being Vertex of G1
for G2 being removeVertex of G1,v st v is isolated holds
G1 is addVertex of G2,v
let v be Vertex of G1; for G2 being removeVertex of G1,v st v is isolated holds
G1 is addVertex of G2,v
let G2 be removeVertex of G1,v; ( v is isolated implies G1 is addVertex of G2,v )
assume A1:
v is isolated
; G1 is addVertex of G2,v
A2:
G1 is Supergraph of G2
by GLIB_006:57;
A3: the_Vertices_of G1 =
((the_Vertices_of G1) \ {v}) \/ {v}
by ZFMISC_1:116
.=
(the_Vertices_of G2) \/ {v}
by GLIB_000:47
;
A4: the_Edges_of G1 =
G1 .edgesBetween (the_Vertices_of G1)
by GLIB_000:34
.=
G1 .edgesBetween ((the_Vertices_of G1) \ {v})
by A1, Th2
.=
the_Edges_of G2
by GLIB_000:47
;
A5: dom (the_Source_of G1) =
the_Edges_of G1
by FUNCT_2:def 1
.=
dom (the_Source_of G2)
by A4, FUNCT_2:def 1
;
for e being object st e in dom (the_Source_of G2) holds
(the_Source_of G2) . e = (the_Source_of G1) . e
by GLIB_000:def 32;
then A6:
the_Source_of G1 = the_Source_of G2
by A5, FUNCT_1:2;
A7: dom (the_Target_of G1) =
the_Edges_of G1
by FUNCT_2:def 1
.=
dom (the_Target_of G2)
by A4, FUNCT_2:def 1
;
for e being object st e in dom (the_Target_of G2) holds
(the_Target_of G2) . e = (the_Target_of G1) . e
by GLIB_000:def 32;
then
the_Target_of G1 = the_Target_of G2
by A7, FUNCT_1:2;
hence
G1 is addVertex of G2,v
by A2, A3, A4, A6, GLIB_006:def 10; verum