theorem Th15: :: FIB_NUM2:15

for i, j being Nat
for x, y being set st 0 < i & i < j holds
{[i,x],[j,y]} is FinSubsequence