let G3 be _Graph; :: thesis: for E being set
for G4 being reverseEdgeDirections of G3,E
for G1 being Supergraph of G3
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is Supergraph of G4
let E be set ; :: thesis: for G4 being reverseEdgeDirections of G3,E
for G1 being Supergraph of G3
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is Supergraph of G4
let G4 be reverseEdgeDirections of G3,E; :: thesis: for G1 being Supergraph of G3
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is Supergraph of G4
let G1 be Supergraph of G3; :: thesis: for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is Supergraph of G4
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( E c= the_Edges_of G3 implies G2 is Supergraph of G4 )
assume A1: E c= the_Edges_of G3 ; :: thesis: G2 is Supergraph of G4
the_Edges_of G3 c= the_Edges_of G1 by GLIB_006:def 9;
then A2: E c= the_Edges_of G1 by A1, XBOOLE_1:1;

now :: thesis: ( the_Vertices_of G4 c= the_Vertices_of G2 & the_Edges_of G4 c= the_Edges_of G2 & ( for e being set st e in the_Edges_of G4 holds
( (the_Source_of G4) . e = (the_Source_of G2) . e & (the_Target_of G4) . e = (the_Target_of G2) . e ) ) )

( the_Vertices_of G2 = the_Vertices_of G1 & the_Vertices_of G3 = the_Vertices_of G4 ) by GLIB_007:4;
hence the_Vertices_of G4 c= the_Vertices_of G2 by GLIB_006:def 9; :: thesis: ( the_Edges_of G4 c= the_Edges_of G2 & ( for e being set st e in the_Edges_of G4 holds
( (the_Source_of G4) . b₂ = (the_Source_of G2) . b₂ & (the_Target_of G4) . b₂ = (the_Target_of G2) . b₂ ) ) )
( the_Edges_of G4 = the_Edges_of G3 & the_Edges_of G2 = the_Edges_of G1 ) by GLIB_007:4;
hence the_Edges_of G4 c= the_Edges_of G2 by GLIB_006:def 9; :: thesis: for e being set st e in the_Edges_of G4 holds
( (the_Source_of G4) . b₂ = (the_Source_of G2) . b₂ & (the_Target_of G4) . b₂ = (the_Target_of G2) . b₂ )
let e be set ; :: thesis: ( e in the_Edges_of G4 implies ( (the_Source_of G4) . b₁ = (the_Source_of G2) . b₁ & (the_Target_of G4) . b₁ = (the_Target_of G2) . b₁ ) )
assume A3: e in the_Edges_of G4 ; :: thesis: ( (the_Source_of G4) . b₁ = (the_Source_of G2) . b₁ & (the_Target_of G4) . b₁ = (the_Target_of G2) . b₁ )
set v4 = (the_Source_of G4) . e;
set w4 = (the_Target_of G4) . e;

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

suppose A4: e in E ; :: thesis: ( (the_Source_of G4) . b₁ = (the_Source_of G2) . b₁ & (the_Target_of G4) . b₁ = (the_Target_of G2) . b₁ )

e DJoins (the_Source_of G4) . e,(the_Target_of G4) . e,G4 by A3, GLIB_000:def 14;
then e DJoins (the_Target_of G4) . e,(the_Source_of G4) . e,G3 by A1, A4, GLIB_007:7;
then e DJoins (the_Target_of G4) . e,(the_Source_of G4) . e,G1 by GLIB_006:70;
then e DJoins (the_Source_of G4) . e,(the_Target_of G4) . e,G2 by A2, A4, GLIB_007:7;
hence ( (the_Source_of G4) . e = (the_Source_of G2) . e & (the_Target_of G4) . e = (the_Target_of G2) . e ) by GLIB_000:def 14; :: thesis: verum

end;

suppose A5: not e in E ; :: thesis: ( (the_Source_of G4) . b₁ = (the_Source_of G2) . b₁ & (the_Target_of G4) . b₁ = (the_Target_of G2) . b₁ )

e DJoins (the_Source_of G4) . e,(the_Target_of G4) . e,G4 by A3, GLIB_000:def 14;
then e DJoins (the_Source_of G4) . e,(the_Target_of G4) . e,G3 by A1, A5, GLIB_007:8;
then e DJoins (the_Source_of G4) . e,(the_Target_of G4) . e,G1 by GLIB_006:70;
then e DJoins (the_Source_of G4) . e,(the_Target_of G4) . e,G2 by A2, A5, GLIB_007:8;
hence ( (the_Source_of G4) . e = (the_Source_of G2) . e & (the_Target_of G4) . e = (the_Target_of G2) . e ) by GLIB_000:def 14; :: thesis: verum

end;

end;

end;

hence G2 is Supergraph of G4 by GLIB_006:def 9; :: thesis: verum