let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is isomorphism )
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is isomorphism )
let G2 be reverseEdgeDirections of G1,E; :: thesis: ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is isomorphism )
reconsider F = id G1 as PGraphMapping of G1,G2 by GLIB_010:12;
take F ; :: thesis: ( F = id G1 & F is isomorphism )
thus F = id G1 ; :: thesis: F is isomorphism
( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 ) ;
then A1: F is total by GLIB_010:def 11;
( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 ) by GLIB_007:4;
then A2: F is onto by GLIB_010:def 12;
( F _V is one-to-one & F _E is one-to-one ) ;
then F is one-to-one by GLIB_010:def 13;
hence F is isomorphism by A1, A2; :: thesis: verum