let G1, G2 be VGraph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 holds

( F is vlabel-preserving iff F " is vlabel-preserving )

let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is vlabel-preserving iff F " is vlabel-preserving )

thus ( F is vlabel-preserving implies F " is vlabel-preserving ) by Th2; :: thesis: ( F " is vlabel-preserving implies F is vlabel-preserving )

( F " is vlabel-preserving implies (F ") " is vlabel-preserving ) by Th2;

hence ( F " is vlabel-preserving implies F is vlabel-preserving ) by Th70; :: thesis: verum

( F is vlabel-preserving iff F " is vlabel-preserving )

let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is vlabel-preserving iff F " is vlabel-preserving )

thus ( F is vlabel-preserving implies F " is vlabel-preserving ) by Th2; :: thesis: ( F " is vlabel-preserving implies F is vlabel-preserving )

( F " is vlabel-preserving implies (F ") " is vlabel-preserving ) by Th2;

hence ( F " is vlabel-preserving implies F is vlabel-preserving ) by Th70; :: thesis: verum