let S1, S2 be Graph-membered set ; :: thesis: ( S1,S2 are_Disomorphic implies ( ( S1 is non-Dmulti implies S2 is non-Dmulti ) & ( S1 is Dsimple implies S2 is Dsimple ) ) )
assume S1,S2 are_Disomorphic ; :: thesis: ( ( S1 is non-Dmulti implies S2 is non-Dmulti ) & ( S1 is Dsimple implies S2 is Dsimple ) )
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: ( S1 is Dsimple implies S2 is Dsimple )

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

now :: thesis: for G2 being _Graph st G2 in S2 holds
G2 is non-Dmulti

let G2 be _Graph; :: thesis: ( G2 in S2 implies G2 is non-Dmulti )
assume G2 in S2 ; :: thesis: G2 is non-Dmulti
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: verum

end;

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

end;

hereby :: thesis: verum

assume A6: S1 is Dsimple ; :: thesis: S2 is Dsimple

now :: thesis: for G2 being _Graph st G2 in S2 holds
G2 is Dsimple

let G2 be _Graph; :: thesis: ( G2 in S2 implies G2 is Dsimple )
assume G2 in S2 ; :: thesis: G2 is Dsimple
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: verum

end;

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

end;