let G1, G2 be _Graph; :: thesis:
let G3 be removeDParallelEdges of G1; :: thesis:
let G4 be removeDParallelEdges of G2; :: thesis:
let G5 be DLGraphComplement of G1; :: thesis:
let G6 be DLGraphComplement of G2; :: thesis:
A1: ( G5 is DLGraphComplement of G3 & G6 is DLGraphComplement of G4 ) by Th47;
assume G4 is G3 -Disomorphic ; :: thesis:
then consider f being directed PVertexMapping of G3,G4 such that
A2: f is Disomorphism by GLIB_011:50;
A3: ( the_Vertices_of G3 = the_Vertices_of G5 & the_Vertices_of G4 = the_Vertices_of G6 ) by A1, Def6;
then reconsider g = f as PartFunc of (the_Vertices_of G5),(the_Vertices_of G6) ;

let v, w, e be object ; :: thesis:
assume A4: ( v in dom g & w in dom g & e DJoins v,w,G5 ) ; :: thesis:
then A5: for e3 being object holds not e3 DJoins v,w,G3 by A1, A3, Def6;
thus ex e6 being object st e6 DJoins g . v,g . w,G6 :: thesis:

assume A6: for e6 being object holds not e6 DJoins g . v,g . w,G6 ; :: thesis:
( g . v in rng f & g . w in rng f ) by A4, FUNCT_1:3;
then consider e4 being object such that
A7: e4 DJoins g . v,g . w,G4 by A1, A6, Def6;
consider e3 being object such that
A8: e3 DJoins v,w,G3 by A2, A4, A7, GLIB_011:def 4;
thus contradiction by A5, A8; :: thesis:

end;

end;

then reconsider g = g as directed PVertexMapping of G5,G6 by GLIB_011:4;

let v, w, e6 be object ; :: thesis:
assume A9: ( v in dom g & w in dom g & e6 DJoins g . v,g . w,G6 ) ; :: thesis:
then ( g . v in rng f & g . w in rng f ) by FUNCT_1:3;
then A10: for e4 being object holds not e4 DJoins g . v,g . w,G4 by A1, A9, Def6;
thus ex e5 being object st e5 DJoins v,w,G5 :: thesis:

assume for e5 being object holds not e5 DJoins v,w,G5 ; :: thesis:
then consider e3 being object such that
A11: e3 DJoins v,w,G3 by A1, A3, A9, Def6;
consider e4 being object such that
A12: e4 DJoins f . v,f . w,G4 by A9, A11, GLIB_011:def 2;
thus contradiction by A10, A12; :: thesis:

end;

end;

then g is Dcontinuous by GLIB_011:def 4;
hence G6 is G5 -Disomorphic by A2, A3, GLIB_011:50; :: thesis: