for X, Y being non empty TopSpace
for N being eventually-directed net of ContMaps (X,(Omega Y))
for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed