for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b