let G3 be _Graph; :: thesis: ( G3 is G2 -isomorphic implies G3 is G1 -isomorphic )
assume G3 is G2 -isomorphic ; :: thesis: G3 is G1 -isomorphic
then consider F2 being PGraphMapping of G2,G3 such that
A1: F2 is isomorphism ;
consider F1 being PGraphMapping of G1,G2 such that
A2: F1 is isomorphism by Def23;
take F2 * F1 ; :: according to GLIB_010:def 23 :: thesis: F2 * F1 is isomorphism
thus F2 * F1 is isomorphism by A1, A2, Th109; :: thesis: verum