let G1 be non _trivial _Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( v is isolated implies G1 is addVertex of G2,v )
assume A1: v is isolated ; :: thesis: 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; :: thesis: verum