let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object holds
( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object holds
( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )
let G1 be reverseEdgeDirections of G2,E; :: thesis: for v1, e, v2 being object holds
( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )

per cases ( E c= the_Edges_of G2 or not E c= the_Edges_of G2 ) ;

suppose A1: E c= the_Edges_of G2 ; :: thesis: for v1, e, v2 being object holds
( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )

let v1, e, v2 be object ; :: thesis: ( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )
thus ( e Joins v1,v2,G2 implies e Joins v1,v2,G1 ) by A1, Lm3; :: thesis: ( e Joins v1,v2,G1 implies e Joins v1,v2,G2 )
reconsider G3 = G2 as reverseEdgeDirections of G1,E by Th3;
assume A2: e Joins v1,v2,G1 ; :: thesis: e Joins v1,v2,G2
E c= the_Edges_of G1 by A1, Def1;
then e Joins v1,v2,G3 by A2, Lm3;
hence e Joins v1,v2,G2 ; :: thesis: verum

end;

suppose not E c= the_Edges_of G2 ; :: thesis: for v1, e, v2 being object holds
( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )

then G1 == G2 by Def1;
hence for v1, e, v2 being object holds
( e Joins v1,v2,G2 iff e Joins v1,v2,G1 ) by GLIB_000:88; :: thesis: verum

end;

end;