:: deftheorem defines ^n FIN_TOPO:def 11 :
for FT being non empty RelStr
for A being Subset of FT holds A ^n = A \ (A ^s);