:: deftheorem defines ^f FIN_TOPO:def 12 :
for FT being non empty RelStr
for A being Subset of FT holds A ^f = { x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y ) } ;