let m, n be Nat; :: thesis: ( n < m implies nat_interval (m,n) = {} )
assume A1: n < m ; :: thesis: nat_interval (m,n) = {}
now :: thesis: for e being object holds not e in nat_interval (m,n)
let e be object ; :: thesis: not e in nat_interval (m,n)
assume e in nat_interval (m,n) ; :: thesis: contradiction
then ex i being Nat st
( e = i & m <= i & i <= n ) ;
hence contradiction by A1, XXREAL_0:2; :: thesis: verum
end;
hence nat_interval (m,n) = {} by XBOOLE_0:def 1; :: thesis: verum