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