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