theorem :: GLIB_015:37
for S1, S2 being Graph-membered set st S1,S2 are_Disomorphic holds
( ( S1 is non-Dmulti implies S2 is non-Dmulti ) & ( S1 is Dsimple implies S2 is Dsimple ) )