let G2, G3 be _Graph; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: ( G2 is addVertices of G4,V implies G2 is reverseEdgeDirections of G1,E )

assume A3: G2 is reverseEdgeDirections of G1,E ; :: thesis: G2 is addVertices of G4,V
then 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 :: thesis: for e, v, w being object st e DJoins v,w,G4 holds
e DJoins v,w,G2

let e, v, w be object ; :: thesis: ( e DJoins v,w,G4 implies b₁ DJoins b₂,b₃,G2 )
assume A6: e DJoins v,w,G4 ; :: thesis: b₁ DJoins b₂,b₃,G2

per cases ( e in E or not e in E ) ;

suppose A7: e in E ; :: thesis: b₁ DJoins b₂,b₃,G2

then 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; :: thesis: verum

end;

suppose A8: not e in E ; :: thesis: b₁ DJoins b₂,b₃,G2

then 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; :: thesis: verum

end;

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; :: thesis: verum

end;

assume A12: G2 is addVertices of G4,V ; :: thesis: G2 is reverseEdgeDirections of G1,E
then 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; :: thesis: verum

end;

suppose A16: not E c= the_Edges_of G3 ; :: thesis: ( G2 is reverseEdgeDirections of G1,E iff G2 is addVertices of G4,V )

then A17: not E c= the_Edges_of G1 by GLIB_006:def 10;
A18: G4 == G3 by A16, GLIB_007:def 1;

hereby :: thesis: ( G2 is addVertices of G4,V implies G2 is reverseEdgeDirections of G1,E )

assume G2 is reverseEdgeDirections of G1,E ; :: thesis: G2 is addVertices of G4,V
then G2 == G1 by A17, GLIB_007:def 1;
then G2 is addVertices of G3,V by GLIB_006:80;
hence G2 is addVertices of G4,V by A18, GLIB_008:32; :: thesis: verum

end;

assume G2 is addVertices of G4,V ; :: thesis: G2 is reverseEdgeDirections of G1,E
then G2 is addVertices of G3,V by A18, GLIB_008:32;
then G1 == G2 by GLIB_006:77;
hence G2 is reverseEdgeDirections of G1,E by A17, GLIB_007:def 1; :: thesis: verum

end;

end;