for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )