:: deftheorem defines ^b FIN_TOPO:def 9 :
for FT being non empty RelStr
for A being Subset of FT holds A ^b = { x where x is Element of FT : U_FT x meets A } ;