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 )

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

hence
id G1 is PGraphMapping of G1,G2
by Th10; :: thesis: verum
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;( 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