:: deftheorem defines Indiscernible T_0TOPSP:def 4 :
for T being non empty TopStruct holds Indiscernible T = Class (Indiscernibility T);