let G1 be _Graph; for V being set
for G2 being removeVertices of G1,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st V c< the_Vertices_of G1 & v1 = v2 holds
( v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V) & v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) )
let V be set ; for G2 being removeVertices of G1,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st V c< the_Vertices_of G1 & v1 = v2 holds
( v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V) & v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) )
let G2 be removeVertices of G1,V; for v1 being Vertex of G1
for v2 being Vertex of G2 st V c< the_Vertices_of G1 & v1 = v2 holds
( v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V) & v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) )
let v1 be Vertex of G1; for v2 being Vertex of G2 st V c< the_Vertices_of G1 & v1 = v2 holds
( v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V) & v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) )
let v2 be Vertex of G2; ( V c< the_Vertices_of G1 & v1 = v2 implies ( v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V) & v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) ) )
assume A1:
( V c< the_Vertices_of G1 & v1 = v2 )
; ( v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V) & v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) )
then A2:
the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V)
by GLIB_000:49;
the_Vertices_of G2 = (the_Vertices_of G1) \ V
by A1, GLIB_000:49;
then A3:
not v2 in V
by XBOOLE_0:def 5;
now for e being object holds
( ( e in v2 .edgesIn() implies e in (v1 .edgesIn()) \ (G1 .edgesOutOf V) ) & ( e in (v1 .edgesIn()) \ (G1 .edgesOutOf V) implies e in v2 .edgesIn() ) )let e be
object ;
( ( e in v2 .edgesIn() implies e in (v1 .edgesIn()) \ (G1 .edgesOutOf V) ) & ( e in (v1 .edgesIn()) \ (G1 .edgesOutOf V) implies e in v2 .edgesIn() ) )assume
e in (v1 .edgesIn()) \ (G1 .edgesOutOf V)
;
e in v2 .edgesIn() then A6:
(
e in v1 .edgesIn() & not
e in G1 .edgesOutOf V )
by XBOOLE_0:def 5;
then A7:
not
(the_Source_of G1) . e in V
by GLIB_000:def 27;
e Joins (the_Source_of G1) . e,
(the_Target_of G1) . e,
G1
by A6, GLIB_000:def 13;
then A8:
(
(the_Source_of G1) . e in the_Vertices_of G1 &
(the_Target_of G1) . e in the_Vertices_of G1 )
by GLIB_000:13;
then
(the_Source_of G1) . e in (the_Vertices_of G1) \ V
by A7, XBOOLE_0:def 5;
then A9:
e in G1 .edgesOutOf ((the_Vertices_of G1) \ V)
by A6, GLIB_000:def 27;
not
(the_Target_of G1) . e in V
by A1, A3, A6, GLIB_000:56;
then
(the_Target_of G1) . e in (the_Vertices_of G1) \ V
by A8, XBOOLE_0:def 5;
then
e in G1 .edgesInto ((the_Vertices_of G1) \ V)
by A6, GLIB_000:def 26;
then A10:
e in the_Edges_of G2
by A2, A9, XBOOLE_0:def 4;
v1 =
(the_Target_of G1) . e
by A6, GLIB_000:56
.=
(the_Target_of G2) . e
by A10, GLIB_000:def 32
;
hence
e in v2 .edgesIn()
by A1, A10, GLIB_000:56;
verum end;
hence A11:
v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V)
by TARSKI:2; ( v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) )
now for e being object holds
( ( e in v2 .edgesOut() implies e in (v1 .edgesOut()) \ (G1 .edgesInto V) ) & ( e in (v1 .edgesOut()) \ (G1 .edgesInto V) implies e in v2 .edgesOut() ) )let e be
object ;
( ( e in v2 .edgesOut() implies e in (v1 .edgesOut()) \ (G1 .edgesInto V) ) & ( e in (v1 .edgesOut()) \ (G1 .edgesInto V) implies e in v2 .edgesOut() ) )assume
e in (v1 .edgesOut()) \ (G1 .edgesInto V)
;
e in v2 .edgesOut() then A14:
(
e in v1 .edgesOut() & not
e in G1 .edgesInto V )
by XBOOLE_0:def 5;
then A15:
not
(the_Target_of G1) . e in V
by GLIB_000:def 26;
e Joins (the_Source_of G1) . e,
(the_Target_of G1) . e,
G1
by A14, GLIB_000:def 13;
then A16:
(
(the_Source_of G1) . e in the_Vertices_of G1 &
(the_Target_of G1) . e in the_Vertices_of G1 )
by GLIB_000:13;
then
(the_Target_of G1) . e in (the_Vertices_of G1) \ V
by A15, XBOOLE_0:def 5;
then A17:
e in G1 .edgesInto ((the_Vertices_of G1) \ V)
by A14, GLIB_000:def 26;
not
(the_Source_of G1) . e in V
by A1, A3, A14, GLIB_000:58;
then
(the_Source_of G1) . e in (the_Vertices_of G1) \ V
by A16, XBOOLE_0:def 5;
then
e in G1 .edgesOutOf ((the_Vertices_of G1) \ V)
by A14, GLIB_000:def 27;
then A18:
e in the_Edges_of G2
by A2, A17, XBOOLE_0:def 4;
v1 =
(the_Source_of G1) . e
by A14, GLIB_000:58
.=
(the_Source_of G2) . e
by A18, GLIB_000:def 32
;
hence
e in v2 .edgesOut()
by A1, A18, GLIB_000:58;
verum end;
hence A19:
v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V)
by TARSKI:2; v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V)
(v1 .edgesOut()) /\ (G1 .edgesOutOf V) = {}
then
v1 .edgesOut() misses G1 .edgesOutOf V
by XBOOLE_0:def 7;
then A21:
(v1 .edgesOut()) \ (G1 .edgesInto V) misses G1 .edgesOutOf V
by XBOOLE_1:36, XBOOLE_1:63;
(v1 .edgesIn()) /\ (G1 .edgesInto V) = {}
then A23:
v1 .edgesIn() misses G1 .edgesInto V
by XBOOLE_0:def 7;
thus v2 .edgesInOut() =
((v1 .edgesIn()) \/ ((v1 .edgesOut()) \ (G1 .edgesInto V))) \ (G1 .edgesOutOf V)
by A11, A19, A21, XBOOLE_1:87
.=
((v1 .edgesInOut()) \ (G1 .edgesInto V)) \ (G1 .edgesOutOf V)
by A23, XBOOLE_1:87
.=
(v1 .edgesInOut()) \ (G1 .edgesInOut V)
by XBOOLE_1:41
; verum