let m, n be Element of NAT ; :: thesis: Seg n misses seq (n,m)

assume Seg n meets seq (n,m) ; :: thesis: contradiction

then consider a being object such that

A1: a in Seg n and

A2: a in seq (n,m) by XBOOLE_0:3;

reconsider i = a as Element of NAT by A1;

( i <= n & n + 1 <= i ) by A1, A2, Th1, FINSEQ_1:1;

hence contradiction by NAT_1:13; :: thesis: verum

assume Seg n meets seq (n,m) ; :: thesis: contradiction

then consider a being object such that

A1: a in Seg n and

A2: a in seq (n,m) by XBOOLE_0:3;

reconsider i = a as Element of NAT by A1;

( i <= n & n + 1 <= i ) by A1, A2, Th1, FINSEQ_1:1;

hence contradiction by NAT_1:13; :: thesis: verum