let G1 be _Graph; :: thesis: for G2 being removeLoops of G1 holds
( G1 is Dcomplete iff G2 is Dcomplete )
let G2 be removeLoops 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 A3: v <> w ; :: thesis: ex e being object st e DJoins v,w,G2
then consider e being object such that
A4: e DJoins v,w,G1 by A1, A2;
take e = e; :: thesis: e DJoins v,w,G2
e Joins v,w,G1 by A4, GLIB_000:16;
then A5: not e in G1 .loops() by A3, GLIB_009:46;
e in the_Edges_of G1 by A4, GLIB_000:def 14;
then e in (the_Edges_of G1) \ (G1 .loops()) by A5, XBOOLE_0:def 5;
then e in the_Edges_of G2 by GLIB_000:53;
hence e DJoins v,w,G2 by A4, 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