for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )