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