let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E holds
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E holds
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )
let G1 be reverseEdgeDirections of G2,E; :: thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

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

suppose E c= the_Edges_of G2 ; :: thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

hence ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by Def1; :: thesis: verum

end;

suppose not E c= the_Edges_of G2 ; :: thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

then G1 == G2 by Def1;
hence ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by GLIB_000:def 34; :: thesis: verum

end;

end;