let G1, G2 be EGraph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 holds
( F is elabel-preserving iff F " is elabel-preserving )
let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is elabel-preserving iff F " is elabel-preserving )
thus ( F is elabel-preserving implies F " is elabel-preserving ) by Th2; :: thesis: ( F " is elabel-preserving implies F is elabel-preserving )
( F " is elabel-preserving implies (F ") " is elabel-preserving ) by Th2;
hence ( F " is elabel-preserving implies F is elabel-preserving ) by Th70; :: thesis: verum