for V being non empty set
for E being set
for S, T being Function of E,V holds
( the_Vertices_of (createGraph (V,E,S,T)) = V & the_Edges_of (createGraph (V,E,S,T)) = E & the_Source_of (createGraph (V,E,S,T)) = S & the_Target_of (createGraph (V,E,S,T)) = T ) by FINSEQ_4:76;