let G1, G2 be _Graph; :: thesis:
assume A1: G1 == G2 ; :: thesis:
then A2: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by Def36;
thus ( G1 is finite implies G2 is finite ) by A2, Def19; :: thesis:

A3: now

assume G1 is loopless ; :: thesis:
then for e being set holds
( not e in the_Edges_of G2 or not (the_Source_of G2) . e = (the_Target_of G2) . e ) by A2, Def20;
hence G2 is loopless by Def20; :: thesis:

end;

hence ( G1 is loopless implies G2 is loopless ) ; :: thesis:

hereby :: thesis:

assume G1 is trivial ; :: thesis:
then card (the_Vertices_of G2) = 1 by A2, Def21;
hence G2 is trivial by Def21; :: thesis:

end;

A4: now

assume A5: G1 is non-multi ; :: thesis:

now

let e1, e2, v1, v2 be set ; :: thesis:
assume ( e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 ) ; :: thesis:
then ( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 ) by A1, Th91;
hence e1 = e2 by A5, Def22; :: thesis:

end;

hence G2 is non-multi by Def22; :: thesis:

end;

hence ( G1 is non-multi implies G2 is non-multi ) ; :: thesis:

A6: now

assume A7: G1 is non-Dmulti ; :: thesis:

now

let e1, e2, v1, v2 be set ; :: thesis:
assume ( e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 ) ; :: thesis:
then ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 ) by A1, Th91;
hence e1 = e2 by A7, Def23; :: thesis:

end;

hence G2 is non-Dmulti by Def23; :: thesis:

end;

hence ( G1 is non-Dmulti implies G2 is non-Dmulti ) ; :: thesis:
thus ( G1 is simple implies G2 is simple ) by A3, A4; :: thesis:
thus ( G1 is Dsimple implies G2 is Dsimple ) by A3, A6; :: thesis: