let G1, G2 be _Graph; :: thesis:
assume A1: G1 == G2 ; :: thesis:
then A2: the_Edges_of G1 = the_Edges_of G2 ;
the_Vertices_of G1 = the_Vertices_of G2 by A1;
hence ( G1 is _finite implies G2 is _finite ) by A2; :: thesis:
A3: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by A1;
A4: ( G1 is loopless implies G2 is loopless ) by A2, A3;
hence ( G1 is loopless implies G2 is loopless ) ; :: thesis:
thus ( G1 is _trivial implies G2 is _trivial ) by A1; :: thesis:

A5: now :: thesis:

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

now :: thesis:

let e1, e2, v1, v2 be object ; :: 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;
hence e1 = e2 by A6; :: thesis:

end;

hence G2 is non-multi ; :: thesis:

end;

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

A7: now :: thesis:

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

now :: thesis:

let e1, e2, v1, v2 be object ; :: 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;
hence e1 = e2 by A8; :: thesis:

end;

hence G2 is non-Dmulti ; :: thesis:

end;

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