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