for X, Y being set
for fs being FinSequence of X
for fss being Subset of fs holds fss | Y is Subset of fs