theorem :: GLIB_015:30
for S1, S2 being Graph-membered set st S1,S2 are_Disomorphic holds
S1,S2 are_isomorphic