:: deftheorem defines T_0-reflex T_0TOPSP:def 5 :
for T being non empty TopSpace holds T_0-reflex T = space (Indiscernible T);