let V be non empty set ; :: thesis: for E being Relation of V holds
( createGraph (V,E) is Dcomplete iff [:V,V:] \ (id V) c= E )
let E be Relation of V; :: thesis: ( createGraph (V,E) is Dcomplete iff [:V,V:] \ (id V) c= E )
set G = createGraph (V,E);

hereby :: thesis: ( [:V,V:] \ (id V) c= E implies createGraph (V,E) is Dcomplete )

assume A1: createGraph (V,E) is Dcomplete ; :: thesis: [:V,V:] \ (id V) c= E

now :: thesis: for v, w being Element of V st [v,w] in [:V,V:] \ (id V) holds
[v,w] in E

let v, w be Element of V; :: thesis: ( [v,w] in [:V,V:] \ (id V) implies [v,w] in E )
assume [v,w] in [:V,V:] \ (id V) ; :: thesis: [v,w] in E
then not [v,w] in id V by XBOOLE_0:def 5;
then A2: v <> w by RELAT_1:def 10;
consider e being object such that
A3: e DJoins v,w, createGraph (V,E) by A1, A2;
e = [v,w] by A3, GLUNIR00:64;
hence [v,w] in E by A3, GLUNIR00:63; :: thesis: verum

end;

hence [:V,V:] \ (id V) c= E by RELSET_1:def 1; :: thesis: verum

end;

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