let G2, G3 be _Graph; for V, E being set
for G1 being addVertices of G3,V
for G4 being reverseEdgeDirections of G3,E holds
( G2 is reverseEdgeDirections of G1,E iff G2 is addVertices of G4,V )
let V, E be set ; for G1 being addVertices of G3,V
for G4 being reverseEdgeDirections of G3,E holds
( G2 is reverseEdgeDirections of G1,E iff G2 is addVertices of G4,V )
let G1 be addVertices of G3,V; for G4 being reverseEdgeDirections of G3,E holds
( G2 is reverseEdgeDirections of G1,E iff G2 is addVertices of G4,V )
let G4 be reverseEdgeDirections of G3,E; ( G2 is reverseEdgeDirections of G1,E iff G2 is addVertices of G4,V )
per cases
( E c= the_Edges_of G3 or not E c= the_Edges_of G3 )
;
suppose A1:
E c= the_Edges_of G3
;
( G2 is reverseEdgeDirections of G1,E iff G2 is addVertices of G4,V )then A2:
E c= the_Edges_of G1
by GLIB_006:def 10;
hereby ( G2 is addVertices of G4,V implies G2 is reverseEdgeDirections of G1,E )
assume A3:
G2 is
reverseEdgeDirections of
G1,
E
;
G2 is addVertices of G4,Vthen A4:
the_Vertices_of G2 =
the_Vertices_of G1
by A2, GLIB_007:def 1
.=
(the_Vertices_of G3) \/ V
by GLIB_006:def 10
.=
(the_Vertices_of G4) \/ V
by A1, GLIB_007:def 1
;
then A5:
the_Vertices_of G4 c= the_Vertices_of G2
by XBOOLE_1:7;
now for e, v, w being object st e DJoins v,w,G4 holds
e DJoins v,w,G2let e,
v,
w be
object ;
( e DJoins v,w,G4 implies b1 DJoins b2,b3,G2 )assume A6:
e DJoins v,
w,
G4
;
b1 DJoins b2,b3,G2per cases
( e in E or not e in E )
;
suppose A7:
e in E
;
b1 DJoins b2,b3,G2then
e DJoins w,
v,
G3
by A1, A6, GLIB_007:7;
then
e DJoins w,
v,
G1
by GLIB_006:85;
hence
e DJoins v,
w,
G2
by A2, A3, A7, GLIB_007:7;
verum end; suppose A8:
not
e in E
;
b1 DJoins b2,b3,G2then
e DJoins v,
w,
G3
by A1, A6, GLIB_007:8;
then
e DJoins v,
w,
G1
by GLIB_006:85;
hence
e DJoins v,
w,
G2
by A2, A3, A8, GLIB_007:8;
verum end; end; then A9:
G2 is
Supergraph of
G4
by A5, Th50;
A10:
the_Edges_of G2 =
the_Edges_of G1
by A2, A3, GLIB_007:def 1
.=
the_Edges_of G3
by GLIB_006:def 10
.=
the_Edges_of G4
by A1, GLIB_007:def 1
;
A11:
the_Source_of G2 =
(the_Source_of G1) +* ((the_Target_of G1) | E)
by A2, A3, GLIB_007:def 1
.=
(the_Source_of G3) +* ((the_Target_of G1) | E)
by GLIB_006:def 10
.=
(the_Source_of G3) +* ((the_Target_of G3) | E)
by GLIB_006:def 10
.=
the_Source_of G4
by A1, GLIB_007:def 1
;
the_Target_of G2 =
(the_Target_of G1) +* ((the_Source_of G1) | E)
by A2, A3, GLIB_007:def 1
.=
(the_Target_of G3) +* ((the_Source_of G1) | E)
by GLIB_006:def 10
.=
(the_Target_of G3) +* ((the_Source_of G3) | E)
by GLIB_006:def 10
.=
the_Target_of G4
by A1, GLIB_007:def 1
;
hence
G2 is
addVertices of
G4,
V
by A4, A9, A10, A11, GLIB_006:def 10;
verum
end; assume A12:
G2 is
addVertices of
G4,
V
;
G2 is reverseEdgeDirections of G1,Ethen A13:
the_Vertices_of G2 =
(the_Vertices_of G4) \/ V
by GLIB_006:def 10
.=
(the_Vertices_of G3) \/ V
by A1, GLIB_007:def 1
.=
the_Vertices_of G1
by GLIB_006:def 10
;
A14:
the_Edges_of G2 =
the_Edges_of G4
by A12, GLIB_006:def 10
.=
the_Edges_of G3
by A1, GLIB_007:def 1
.=
the_Edges_of G1
by GLIB_006:def 10
;
A15:
the_Source_of G2 =
the_Source_of G4
by A12, GLIB_006:def 10
.=
(the_Source_of G3) +* ((the_Target_of G3) | E)
by A1, GLIB_007:def 1
.=
(the_Source_of G1) +* ((the_Target_of G3) | E)
by GLIB_006:def 10
.=
(the_Source_of G1) +* ((the_Target_of G1) | E)
by GLIB_006:def 10
;
the_Target_of G2 =
the_Target_of G4
by A12, GLIB_006:def 10
.=
(the_Target_of G3) +* ((the_Source_of G3) | E)
by A1, GLIB_007:def 1
.=
(the_Target_of G1) +* ((the_Source_of G3) | E)
by GLIB_006:def 10
.=
(the_Target_of G1) +* ((the_Source_of G1) | E)
by GLIB_006:def 10
;
hence
G2 is
reverseEdgeDirections of
G1,
E
by A2, A13, A14, A15, GLIB_007:def 1;
verum end;