set G = createGraph (V,E,S,T);
the_Edges_of (createGraph (V,E,S,T)) = E by FINSEQ_4:91;
then for e1, e2, v1, v2 being set st e1 Joins v1,v2, createGraph (V,E,S,T) & e2 Joins v1,v2, createGraph (V,E,S,T) holds
e1 = e2 by Def15;
then A1: createGraph (V,E,S,T) is non-multi by Def22;
for e being set 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:91;
then createGraph (V,E,S,T) is loopless by Def20;
hence createGraph (V,E,S,T) is simple by A1; :: thesis: verum