let G be _Graph; for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
let v be object ; for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
let V be set ; for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
let G1 be addAdjVertexToAll of G,v,V; for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
let G2 be addAdjVertexFromAll of G,v,V; ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} ) )
set E = V --> (the_Edges_of G);
assume A1:
( V c= the_Vertices_of G & not v in the_Vertices_of G )
; ( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
then A2:
( G1 .edgesOutOf {v} = V --> (the_Edges_of G) & G2 .edgesInto {v} = V --> (the_Edges_of G) )
by Th33, Th34;
A3:
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & the_Edges_of G1 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G1 = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of G1 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) )
by A1, Def2;
A4:
( the_Vertices_of G2 = (the_Vertices_of G) \/ {v} & the_Edges_of G2 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G2 = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of G2 = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) )
by A1, Def3;
A5:
dom ((V --> (the_Edges_of G)) --> v) = V --> (the_Edges_of G)
;
A6: dom (pr1 (V,{(the_Edges_of G)})) =
[:V,{(the_Edges_of G)}:]
by FUNCT_3:def 4
.=
V --> (the_Edges_of G)
by FUNCOP_1:def 2
;
A9: the_Source_of G2 =
(the_Source_of G1) +* ((pr1 (V,{(the_Edges_of G)})) | (V --> (the_Edges_of G)))
by A3, A4, A5, A6, FUNCT_4:74
.=
(the_Source_of G1) +* ((the_Target_of G1) | (V --> (the_Edges_of G)))
by A6, A3
;
A11: the_Target_of G2 =
(the_Target_of G1) +* (((V --> (the_Edges_of G)) --> v) | (V --> (the_Edges_of G)))
by A3, A4, A5, A6, FUNCT_4:74
.=
(the_Target_of G1) +* ((the_Source_of G1) | (V --> (the_Edges_of G)))
by A5, A3
;
A13: the_Source_of G1 =
(the_Source_of G2) +* (((V --> (the_Edges_of G)) --> v) | (V --> (the_Edges_of G)))
by A3, A4, A5, A6, FUNCT_4:74
.=
(the_Source_of G2) +* ((the_Target_of G2) | (V --> (the_Edges_of G)))
by A5, A4
;
A15: the_Target_of G1 =
(the_Target_of G2) +* ((pr1 (V,{(the_Edges_of G)})) | (V --> (the_Edges_of G)))
by A3, A4, A5, A6, FUNCT_4:74
.=
(the_Target_of G2) +* ((the_Source_of G2) | (V --> (the_Edges_of G)))
by A6, A4
;
thus
G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v}
by A2, A3, A4, A9, A11, Def1; G1 is reverseEdgeDirections of G2,G2 .edgesInto {v}
thus
G1 is reverseEdgeDirections of G2,G2 .edgesInto {v}
by A2, A3, A4, A13, A15, Def1; verum