set G = createGraph V,E,S,T;
( the_Vertices_of (createGraph V,E,S,T) = V & the_Edges_of (createGraph V,E,S,T) = E ) by FINSEQ_4:91;
hence createGraph V,E,S,T is finite by Def19; :: thesis: verum