theorem :: GLIB_010:99

for G1 being _Graph
for G2 being b₁ -Disomorphic _Graph
for G3 being b₂ -Disomorphic _Graph
for F being DIsomorphism of G1,G2 st G1 == G3 holds
F " is DIsomorphism of G2,G3