let m, n be Element of NAT ; :: thesis: ( n < m implies nat_interval (m,n) = {} )
assume A1: n < m ; :: thesis: nat_interval (m,n) = {}

now

let e be set ; :: thesis: not e in nat_interval (m,n)
assume e in nat_interval (m,n) ; :: thesis: contradiction
then ex i being Element of 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