let S1, S2 be Graph-membered set ; :: thesis:
assume S1,S2 are_Disomorphic ; :: thesis:
then consider f being one-to-one Function such that
A1: ( dom f = S1 & rng f = S2 ) and
A2: for G being _Graph st G in S1 holds
f . G is b₁ -Disomorphic _Graph ;

hereby :: thesis:

assume A3: S1 is non-Dmulti ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A4: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A4;
G2 is G1 -Disomorphic by A1, A2, A4;
then consider G being PGraphMapping of G1,G2 such that
A5: G is Disomorphism by GLIB_010:def 24;
thus G2 is non-Dmulti by A1, A3, A4, A5, GLIB_010:90; :: thesis:

end;

hence S2 is non-Dmulti by GLIB_014:def 5; :: thesis:

end;

hereby :: thesis:

assume A6: S1 is Dsimple ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A7: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A7;
G2 is G1 -Disomorphic by A1, A2, A7;
then consider G being PGraphMapping of G1,G2 such that
A8: G is Disomorphism by GLIB_010:def 24;
thus G2 is Dsimple by A1, A6, A7, A8, GLIB_010:90; :: thesis:

end;

hence S2 is Dsimple by GLIB_014:def 7; :: thesis:

end;