let n1, m1, n2, m2 be Nat; :: thesis: ( n1 + m1 <= n2 implies seq (n1,m1) misses seq (n2,m2) )
assume A1: n1 + m1 <= n2 ; :: thesis: seq (n1,m1) misses seq (n2,m2)
assume seq (n1,m1) meets seq (n2,m2) ; :: thesis: contradiction
then consider x being object such that
A2: ( x in seq (n1,m1) & x in seq (n2,m2) ) by XBOOLE_0:3;
reconsider x = x as Nat by A2;
( n2 < x & x <= n1 + m1 ) by A2, Th73;
hence contradiction by A1, XXREAL_0:2; :: thesis: verum