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