let G1 be _Graph; for v, e being set
for G2 being removeEdge of G1,e
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeEdge of G3,e
let v, e be set ; for G2 being removeEdge of G1,e
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeEdge of G3,e
let G2 be removeEdge of G1,e; for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeEdge of G3,e
let G3 be removeVertex of G1,v; for G4 being removeVertex of G2,v holds G4 is removeEdge of G3,e
let G4 be removeVertex of G2,v; G4 is removeEdge of G3,e
A1:
( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} )
by GLIB_000:51;
per cases
( ( not G1 is _trivial & v in the_Vertices_of G1 ) or G1 is _trivial or not v in the_Vertices_of G1 )
;
suppose A2:
( not
G1 is
_trivial &
v in the_Vertices_of G1 )
;
G4 is removeEdge of G3,ethen reconsider v1 =
v as
Vertex of
G1 ;
reconsider v2 =
v1 as
Vertex of
G2 by A1;
(
the_Vertices_of G3 = (the_Vertices_of G1) \ {v} &
the_Edges_of G3 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) )
by A2, GLIB_000:47;
then A3:
the_Edges_of G3 =
(G1 .edgesBetween (the_Vertices_of G1)) \ (v1 .edgesInOut())
by Th1
.=
(the_Edges_of G1) \ (v1 .edgesInOut())
by GLIB_000:34
;
(
the_Vertices_of G4 = (the_Vertices_of G2) \ {v} &
the_Edges_of G4 = G2 .edgesBetween ((the_Vertices_of G2) \ {v}) )
by A1, A2, GLIB_000:47;
then A4:
the_Edges_of G4 =
(G2 .edgesBetween (the_Vertices_of G2)) \ (v2 .edgesInOut())
by Th1
.=
(the_Edges_of G2) \ (v2 .edgesInOut())
by GLIB_000:34
;
A5:
the_Vertices_of G4 =
(the_Vertices_of G1) \ {v}
by A1, A2, GLIB_000:47
.=
the_Vertices_of G3
by A2, GLIB_000:47
;
for
x being
object st
x in the_Edges_of G4 holds
x in (the_Edges_of G3) \ {e}
then A8:
the_Edges_of G4 c= (the_Edges_of G3) \ {e}
by TARSKI:def 3;
(the_Edges_of G3) \ {e} c= the_Edges_of G3
by XBOOLE_1:36;
then A9:
the_Edges_of G4 c= the_Edges_of G3
by A8, XBOOLE_1:1;
G4 is
Subgraph of
G1
by GLIB_000:43;
then A10:
G4 is
Subgraph of
G3
by A5, A9, GLIB_000:44;
hence
G4 is
removeEdge of
G3,
e
by A10, A11, GLIB_000:def 37;
verum end; end;