Description: The indiscrete topology on a set A expressed as a topological space,
using implicit structure indices. The advantage of this version over
indistpsx is that it is independent of the indices of the component
definitions df-base and df-tset , and if they are changed in the
future, this theorem will not be affected. The advantage over
indistps2 is that it is easy to eliminate the hypotheses with eqid and vtoclg to result in a closed theorem. Theorems indistpsALT and
indistps2ALT show that the two forms can be derived from each other.
(Contributed by FL, 19-Jul-2006)