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

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