A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union, see toponuni), and it may sometimes be more convenient to consider topologies without reference to the underlying set. This is why we define successively the class of topologies (df-top), then the function which associates with a set the set of topologies on it (df-topon), and finally the class of topological spaces, as extensible structures having an underlying set and a topology on it (df-topsp). Of course, a topology is the same thing as a topology on a set (see toprntopon).