for p being FinSequence
for x being set
for n being Nat st x in rng p & n in dom p & p is one-to-one holds
( x in p .followSet n iff x .. p >= n )