theorem Th27: :: GRAPH_2:27

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