thus ( canDCompleteGraph c is plain & canDCompleteGraph c is c -vertex ) ; :: thesis: ( canDCompleteGraph c is Dsimple & canDCompleteGraph c is Dcomplete )
[:c,c:] \ (id c) misses id c by XBOOLE_1:79;
then [:c,c:] \ (id c) is irreflexive by GLIBPRE0:11;
hence canDCompleteGraph c is Dsimple ; :: thesis: canDCompleteGraph c is Dcomplete

now :: thesis: for v, w being Vertex of (canDCompleteGraph c) st v <> w holds
ex e being object st e DJoins v,w, canDCompleteGraph c

let v, w be Vertex of (canDCompleteGraph c); :: thesis: ( v <> w implies ex e being object st e DJoins v,w, canDCompleteGraph c )
assume v <> w ; :: thesis: ex e being object st e DJoins v,w, canDCompleteGraph c
then A2: not [v,w] in id c by RELAT_1:def 10;
reconsider e = [v,w] as object ;
take e = e; :: thesis: e DJoins v,w, canDCompleteGraph c
[v,w] in [:c,c:] \ (id c) by A2, XBOOLE_0:def 5;
hence e DJoins v,w, canDCompleteGraph c by GLUNIR00:63; :: thesis: verum

end;

hence canDCompleteGraph c is Dcomplete ; :: thesis: verum