let k, m, n be Element of NAT ; :: thesis: ( k < m implies Seg k misses nat_interval m,n )
assume A1: k < m ; :: thesis: Seg k misses nat_interval m,n

now

let e be set ; :: thesis: ( e in (Seg k) /\ (nat_interval m,n) implies e in {} )
assume e in (Seg k) /\ (nat_interval m,n) ; :: thesis: e in {}
then A2: ( e in Seg k & e in nat_interval m,n ) by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A3: ( e = i & 1 <= i & i <= k ) by Lm1;
consider j being Element of NAT such that
A4: ( e = j & m <= j & j <= n ) by A2;
thus e in {} by A1, A3, A4, XXREAL_0:2; :: thesis: verum

end;

then (Seg k) /\ (nat_interval m,n) c= {} by TARSKI:def 3;
then (Seg k) /\ (nat_interval m,n) = {} ;
hence Seg k misses nat_interval m,n by XBOOLE_0:def 7; :: thesis: verum