let i, j be Nat; :: thesis: for x, y being set st 0 < i & i < j holds
{[i,x],[j,y]} is FinSubsequence
let x, y be set ; :: thesis: ( 0 < i & i < j implies {[i,x],[j,y]} is FinSubsequence )
assume A1: ( 0 < i & i < j ) ; :: thesis: {[i,x],[j,y]} is FinSubsequence
then reconsider X = {[i,x],[j,y]} as Function by GRFUNC_1:19;
A2: 0 + 1 <= i by A1, NAT_1:13;
X is FinSubsequence-like

proof

A3: dom X = {i,j} by RELAT_1:24;
{i,j} c= Seg j

proof

now

let x be set ; :: thesis: ( x in {i,j} implies x in Seg j )
assume x in {i,j} ; :: thesis: x in Seg j
then X: ( x = i or x = j ) by TARSKI:def 2;
i in NAT by ORDINAL1:def 13;
hence x in Seg j by A1, A2, X, FINSEQ_1:5; :: thesis: verum

end;

hence {i,j} c= Seg j by TARSKI:def 3; :: thesis: verum

end;

hence X is FinSubsequence-like by A3, FINSEQ_1:def 12; :: thesis: verum

end;

hence {[i,x],[j,y]} is FinSubsequence ; :: thesis: verum