:: deftheorem defines ^d FINTOPO3:def 1 :
for T being non empty RelStr
for A being Subset of T holds A ^d = { x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y } ;