set IT = { i where i is Element of NAT : ( m <= i & i <= n ) } ;

now

let e be set ; :: thesis: ( e in { i where i is Element of NAT : ( m <= i & i <= n ) } implies e in {0 } \/ (Seg n) )
assume e in { i where i is Element of NAT : ( m <= i & i <= n ) } ; :: thesis: e in {0 } \/ (Seg n)
then consider i being Element of NAT such that
A1: i = e and
m <= i and
A2: i <= n ;

now

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: e in {0 } \/ (Seg n)

then i in {0 } by TARSKI:def 1;
hence e in {0 } \/ (Seg n) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: e in {0 } \/ (Seg n)

then 0 + 1 <= i by NAT_1:13;
then e in Seg n by A1, A2, FINSEQ_1:3;
hence e in {0 } \/ (Seg n) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence e in {0 } \/ (Seg n) ; :: thesis: verum

end;

then { i where i is Element of NAT : ( m <= i & i <= n ) } c= {0 } \/ (Seg n) by TARSKI:def 3;
hence nat_interval m,n is finite ; :: thesis: verum