for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )