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 A2: e in (Seg k) /\ (nat_interval m,n) ; :: thesis: e in {}
then e in nat_interval m,n by XBOOLE_0:def 4;
then A3: ex j being Element of NAT st
( e = j & m <= j & j <= n ) ;
e in Seg k by A2, XBOOLE_0:def 4;
then ex i being Element of NAT st
( e = i & 1 <= i & i <= k ) by Lm1;
hence e in {} by A1, A3, 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