let G be _Graph; :: thesis: ( G is Dcomplete iff [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) c= VertexDomRel G )
set V = the_Vertices_of G;

hereby :: thesis: ( [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) c= VertexDomRel G implies G is Dcomplete )

assume A1: G is Dcomplete ; :: thesis: [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) c= VertexDomRel G

now :: thesis: for v, w being Vertex of G st [v,w] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) holds
[v,w] in VertexDomRel G

let v, w be Vertex of G; :: thesis: ( [v,w] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) implies [v,w] in VertexDomRel G )
assume [v,w] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) ; :: thesis: [v,w] in VertexDomRel G
then not [v,w] in id (the_Vertices_of G) by XBOOLE_0:def 5;
then v <> w by RELAT_1:def 10;
then ex e being object st e DJoins v,w,G by A1;
hence [v,w] in VertexDomRel G by GLUNIR00:1; :: thesis: verum

end;

hence [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) c= VertexDomRel G by RELSET_1:def 1; :: thesis: verum

end;

assume A2: [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) c= VertexDomRel G ; :: thesis: G is Dcomplete
let v, w be Vertex of G; :: according to GLIB_016:def 1 :: thesis: ( v <> w implies ex e being object st e DJoins v,w,G )
assume v <> w ; :: thesis: ex e being object st e DJoins v,w,G
then not [v,w] in id (the_Vertices_of G) by RELAT_1:def 10;
then [v,w] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) by XBOOLE_0:def 5;
hence ex e being object st e DJoins v,w,G by A2, GLUNIR00:1; :: thesis: verum