let k, m, n be 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 :: thesis: for e being object st e in (Seg k) /\ (nat_interval (m,n)) holds
e in {}
let e be object ; :: 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 Nat st
( e = j & m <= j & j <= n ) ;
e in Seg k by A2, XBOOLE_0:def 4;
then ex i being Nat st
( e = i & 1 <= i & i <= k ) ;
hence e in {} by A1, A3, XXREAL_0:2; :: thesis: verum
end;
then (Seg k) /\ (nat_interval (m,n)) c= {} ;
then (Seg k) /\ (nat_interval (m,n)) = {} ;
hence Seg k misses nat_interval (m,n) by XBOOLE_0:def 7; :: thesis: verum