theorem Th16: :: FIB_NUM2:16

for i, j being Nat
for x, y being set
for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds
Seq q = <*x,y*>