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

A5: 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, A4, 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 A3, Def21;
hence G2 is trivial by Def21; :: thesis:

end;

A6: now

assume A7: 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 A7, Def22; :: thesis:

end;

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

end;

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

A8: now

assume A9: 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 A9, 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 A5, A6; :: thesis:
thus ( G1 is Dsimple implies G2 is Dsimple ) by A5, A8; :: thesis: