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

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