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; :: thesis: verum