set G = createGraph (V,E,S,T);
for e1, e2, v1, v2 being object st e1 Joins v1,v2, createGraph (V,E,S,T) & e2 Joins v1,v2, createGraph (V,E,S,T) holds
e1 = e2
;
then A1:
createGraph (V,E,S,T) is non-multi
;
createGraph (V,E,S,T) is loopless
;
hence
createGraph (V,E,S,T) is simple
by A1; verum