let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1 holds
( G1 is Dcomplete iff G2 is Dcomplete )
let G2 be removeDParallelEdges of G1; :: thesis: ( G1 is Dcomplete iff G2 is Dcomplete )

hereby :: thesis: ( G2 is Dcomplete implies G1 is Dcomplete )

assume A1: G1 is Dcomplete ; :: thesis: G2 is Dcomplete

now :: thesis: for v, w being Vertex of G2 st v <> w holds
ex e being object st e DJoins v,w,G2

let v, w be Vertex of G2; :: thesis: ( v <> w implies ex e being object st e DJoins v,w,G2 )
A2: ( v is Vertex of G1 & w is Vertex of G1 ) by GLIB_000:def 33;
assume v <> w ; :: thesis: ex e being object st e DJoins v,w,G2
then consider e0 being object such that
A3: e0 DJoins v,w,G1 by A1, A2;
consider E being RepDEdgeSelection of G1 such that
A4: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by GLIB_009:def 8;
consider e being object such that
A5: ( e DJoins v,w,G1 & e in E ) and
for e9 being object st e9 DJoins v,w,G1 & e9 in E holds
e9 = e by A3, GLIB_009:def 6;
take e = e; :: thesis: e DJoins v,w,G2
the_Vertices_of G1 c= the_Vertices_of G1 ;
then ( the_Vertices_of G1 is non empty Subset of (the_Vertices_of G1) & G1 .edgesBetween (the_Vertices_of G1) = the_Edges_of G1 ) by GLIB_000:34;
then the_Edges_of G2 = E by A4, GLIB_000:def 37;
hence e DJoins v,w,G2 by A5, GLIB_000:73; :: thesis: verum

end;

hence G2 is Dcomplete ; :: thesis: verum

end;

assume A6: G2 is Dcomplete ; :: thesis: G1 is Dcomplete
let v, w be Vertex of G1; :: according to GLIB_016:def 1 :: thesis: ( v <> w implies ex e being object st e DJoins v,w,G1 )
A7: ( v is Vertex of G2 & w is Vertex of G2 ) by GLIB_000:def 33;
assume v <> w ; :: thesis: ex e being object st e DJoins v,w,G1
then consider e being object such that
A8: e DJoins v,w,G2 by A6, A7;
take e ; :: thesis: e DJoins v,w,G1
thus e DJoins v,w,G1 by A8, GLIB_000:72; :: thesis: verum