let a, b be Nat; :: thesis: Seg a misses seq (a,b)
assume Seg a meets seq (a,b) ; :: thesis: contradiction
then consider a1 being object such that
A1: a1 in Seg a and
A2: a1 in seq (a,b) by XBOOLE_0:3;
reconsider i = a1 as Element of NAT by A1;
( i <= a & a + 1 <= i ) by A1, A2, Th1, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum