let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E holds
( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E holds
( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )
thus id G1 = [(id (the_Vertices_of G2)),(id (the_Edges_of G1))] by GLIB_007:4
.= id G2 by GLIB_007:4 ; :: thesis: id G1 is PGraphMapping of G1,G2
ex E1, E2 being set st
( G1 is reverseEdgeDirections of G1,E1 & G2 is reverseEdgeDirections of G1,E2 )

proof

take {} ; :: thesis: ex E2 being set st
( G1 is reverseEdgeDirections of G1, {} & G2 is reverseEdgeDirections of G1,E2 )
take E ; :: thesis: ( G1 is reverseEdgeDirections of G1, {} & G2 is reverseEdgeDirections of G1,E )
thus ( G1 is reverseEdgeDirections of G1, {} & G2 is reverseEdgeDirections of G1,E ) by GLIB_009:43; :: thesis: verum

end;

hence id G1 is PGraphMapping of G1,G2 by Th10; :: thesis: verum