let G1 be _Graph; :: thesis: for G2 being DSimpleGraph of G1 holds
( G1 is Dcomplete iff G2 is Dcomplete )
let G2 be DSimpleGraph of G1; :: thesis: ( G1 is Dcomplete iff G2 is Dcomplete )
consider G9 being removeDParallelEdges of G1 such that
A1: G2 is removeLoops of G9 by GLIB_009:120;

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

assume G1 is Dcomplete ; :: thesis: G2 is Dcomplete
then G9 is Dcomplete by Th6;
hence G2 is Dcomplete by A1, Th5; :: thesis: verum

end;

assume G2 is Dcomplete ; :: thesis: G1 is Dcomplete
then G9 is Dcomplete by A1, Th5;
hence G1 is Dcomplete by Th6; :: thesis: verum