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