let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies G2 is G1 -Disomorphic )
assume G1 == G2 ; :: thesis: G2 is G1 -Disomorphic
then consider F being PGraphMapping of G1,G2 such that
A1: ( F = id G1 & F is Disomorphism ) by Th81;
thus G2 is G1 -Disomorphic by A1, GLIB_010:def 24; :: thesis: verum