let G2, G3 be _Graph; for v, e, w being object
for G1 being addAdjVertex of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addAdjVertex of G3,w,e,v )
let v, e, w be object ; for G1 being addAdjVertex of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addAdjVertex of G3,w,e,v )
let G1 be addAdjVertex of G3,v,e,w; ( not e in the_Edges_of G3 implies ( G2 is reverseEdgeDirections of G1,{e} iff G2 is addAdjVertex of G3,w,e,v ) )
assume A1:
not e in the_Edges_of G3
; ( G2 is reverseEdgeDirections of G1,{e} iff G2 is addAdjVertex of G3,w,e,v )
per cases
( ( v in the_Vertices_of G3 & not w in the_Vertices_of G3 ) or ( not v in the_Vertices_of G3 & w in the_Vertices_of G3 ) or ( not ( v in the_Vertices_of G3 & not w in the_Vertices_of G3 ) & not ( not v in the_Vertices_of G3 & w in the_Vertices_of G3 ) ) )
;
suppose A2:
(
v in the_Vertices_of G3 & not
w in the_Vertices_of G3 )
;
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addAdjVertex of G3,w,e,v )then consider G4 being
addVertex of
G3,
w such that A3:
G1 is
addEdge of
G4,
v,
e,
w
by A1, GLIB_006:125;
A4:
the_Edges_of G4 = the_Edges_of G3
by GLIB_006:def 10;
hereby ( G2 is addAdjVertex of G3,w,e,v implies G2 is reverseEdgeDirections of G1,{e} )
assume
G2 is
reverseEdgeDirections of
G1,
{e}
;
G2 is addAdjVertex of G3,w,e,vthen
G2 is
addEdge of
G4,
w,
e,
v
by A1, A3, A4, Th66;
hence
G2 is
addAdjVertex of
G3,
w,
e,
v
by A1, A2, GLIB_006:128;
verum
end; assume
G2 is
addAdjVertex of
G3,
w,
e,
v
;
G2 is reverseEdgeDirections of G1,{e}then consider G5 being
addVertex of
G3,
w such that A5:
G2 is
addEdge of
G5,
w,
e,
v
by A1, A2, GLIB_006:126;
G2 is
addEdge of
G4,
w,
e,
v
by A5, GLIB_006:77, GLIB_008:36;
hence
G2 is
reverseEdgeDirections of
G1,
{e}
by A1, A3, A4, Th66;
verum end; suppose A6:
( not
v in the_Vertices_of G3 &
w in the_Vertices_of G3 )
;
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addAdjVertex of G3,w,e,v )then consider G4 being
addVertex of
G3,
v such that A7:
G1 is
addEdge of
G4,
v,
e,
w
by A1, GLIB_006:126;
A8:
the_Edges_of G4 = the_Edges_of G3
by GLIB_006:def 10;
hereby ( G2 is addAdjVertex of G3,w,e,v implies G2 is reverseEdgeDirections of G1,{e} )
assume
G2 is
reverseEdgeDirections of
G1,
{e}
;
G2 is addAdjVertex of G3,w,e,vthen
G2 is
addEdge of
G4,
w,
e,
v
by A1, A7, A8, Th66;
hence
G2 is
addAdjVertex of
G3,
w,
e,
v
by A1, A6, GLIB_006:127;
verum
end; assume
G2 is
addAdjVertex of
G3,
w,
e,
v
;
G2 is reverseEdgeDirections of G1,{e}then consider G5 being
addVertex of
G3,
v such that A9:
G2 is
addEdge of
G5,
w,
e,
v
by A1, A6, GLIB_006:125;
G2 is
addEdge of
G4,
w,
e,
v
by A9, GLIB_006:77, GLIB_008:36;
hence
G2 is
reverseEdgeDirections of
G1,
{e}
by A1, A7, A8, Th66;
verum end; suppose A10:
( not (
v in the_Vertices_of G3 & not
w in the_Vertices_of G3 ) & not ( not
v in the_Vertices_of G3 &
w in the_Vertices_of G3 ) )
;
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addAdjVertex of G3,w,e,v )then A11:
G1 == G3
by GLIB_006:def 12;
then
the_Edges_of G1 = the_Edges_of G3
by GLIB_000:def 34;
then A12:
not
{e} c= the_Edges_of G1
by A1, ZFMISC_1:31;
hereby ( G2 is addAdjVertex of G3,w,e,v implies G2 is reverseEdgeDirections of G1,{e} )
assume
G2 is
reverseEdgeDirections of
G1,
{e}
;
G2 is addAdjVertex of G3,w,e,vthen
G2 == G1
by A12, GLIB_007:def 1;
then A13:
G2 == G3
by A11, GLIB_000:85;
then
G2 is
Supergraph of
G3
by GLIB_006:59;
hence
G2 is
addAdjVertex of
G3,
w,
e,
v
by A10, A13, GLIB_006:def 12;
verum
end; assume
G2 is
addAdjVertex of
G3,
w,
e,
v
;
G2 is reverseEdgeDirections of G1,{e}then
G2 == G3
by A10, GLIB_006:def 12;
then
G2 == G1
by A11, GLIB_000:85;
hence
G2 is
reverseEdgeDirections of
G1,
{e}
by A12, GLIB_007:def 1;
verum end;