let G3 be _Graph; :: thesis: ( G3 is G2 -Disomorphic implies G3 is G1 -Disomorphic )
assume G3 is G2 -Disomorphic ; :: thesis: G3 is G1 -Disomorphic
then consider F2 being PGraphMapping of G2,G3 such that
A1: F2 is Disomorphism ;
reconsider F2 = F2 as directed PGraphMapping of G2,G3 by A1;
consider F1 being PGraphMapping of G1,G2 such that
A2: F1 is Disomorphism by Def24;
reconsider F1 = F1 as directed PGraphMapping of G1,G2 by A2;
take F2 * F1 ; :: according to GLIB_010:def 24 :: thesis: F2 * F1 is Disomorphism
thus F2 * F1 is Disomorphism by A1, A2, Th110; :: thesis: verum