set G0 = createGraph (V,E);
thus createGraph (V,E) is plain ; :: thesis: createGraph (V,E) is non-Dmulti
now :: thesis: for e1, e2, v, w being object st e1 DJoins v,w, createGraph (V,E) & e2 DJoins v,w, createGraph (V,E) holds
e1 = e2
let e1, e2, v, w be object ; :: thesis: ( e1 DJoins v,w, createGraph (V,E) & e2 DJoins v,w, createGraph (V,E) implies e1 = e2 )
assume ( e1 DJoins v,w, createGraph (V,E) & e2 DJoins v,w, createGraph (V,E) ) ; :: thesis: e1 = e2
then ( e1 = [v,w] & e2 = [v,w] ) by Th64;
hence e1 = e2 ; :: thesis: verum
end;
hence createGraph (V,E) is non-Dmulti by GLIB_000:def 21; :: thesis: verum