for x being set st x in rng (X --> T) holds
x is TopSpace by TARSKI:def 1;
hence X --> T is TopSpace-yielding ; :: thesis: verum