set G = createGraph V,E,S,T;
A1: ( the_Vertices_of (createGraph V,E,S,T) = V & the_Edges_of (createGraph V,E,S,T) = E ) by FINSEQ_4:91;
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 A2: createGraph V,E,S,T is loopless by Def20;
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 A1, Def15;
then createGraph V,E,S,T is non-multi by Def22;
hence createGraph V,E,S,T is simple by A2; :: thesis: verum