let G be _Graph; :: thesis: ( G is Dcomplete implies G is complete )
assume A1: G is Dcomplete ; :: thesis: G is complete

now :: thesis: for v, w being Vertex of G st v <> w holds
v,w are_adjacent

let v, w be Vertex of G; :: thesis: ( v <> w implies v,w are_adjacent )
assume v <> w ; :: thesis: v,w are_adjacent
then consider e being object such that
A2: e DJoins v,w,G by A1;
e Joins v,w,G by A2, GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

hence G is complete by CHORD:def 6; :: thesis: verum