set G = createGraph (V,E,S,T);
the_Edges_of (createGraph (V,E,S,T)) = E
by FINSEQ_4:76;
then
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
;
for e being object holds
( not e in the_Edges_of (createGraph (V,E,S,T)) or not (the_Source_of (createGraph (V,E,S,T))) . e = (the_Target_of (createGraph (V,E,S,T))) . e )
by FINSEQ_4:76;
then
createGraph (V,E,S,T) is loopless
;
hence
createGraph (V,E,S,T) is simple
by A1; verum