let G1 be _Graph; :: thesis: for G2 being G1 -Disomorphic _Graph holds G1 is G2 -Disomorphic

let G2 be G1 -Disomorphic _Graph; :: thesis: G1 is G2 -Disomorphic

consider F being PGraphMapping of G1,G2 such that

A1: F is Disomorphism by Def24;

reconsider F = F as one-to-one Dcontinuous PGraphMapping of G1,G2 by A1;

take F " ; :: according to GLIB_010:def 24 :: thesis: F " is Disomorphism

thus F " is Disomorphism by A1, Th71, Th72; :: thesis: verum

let G2 be G1 -Disomorphic _Graph; :: thesis: G1 is G2 -Disomorphic

consider F being PGraphMapping of G1,G2 such that

A1: F is Disomorphism by Def24;

reconsider F = F as one-to-one Dcontinuous PGraphMapping of G1,G2 by A1;

take F " ; :: according to GLIB_010:def 24 :: thesis: F " is Disomorphism

thus F " is Disomorphism by A1, Th71, Th72; :: thesis: verum