:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def 3 :
for T being non empty TopStruct
for b2 being Equivalence_Relation of the carrier of T holds
( b2 = Indiscernibility T iff for p, q being Point of T holds
( [p,q] in b2 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) );