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:1;
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 A3: { i where i is Element of NAT : ( m <= i & i <= n ) } c= {0} \/ (Seg n) by TARSKI:def 3;
{0} c= NAT by ZFMISC_1:31;
then {0} \/ (Seg n) c= NAT by XBOOLE_1:8;
hence { i where i is Element of NAT : ( m <= i & i <= n ) } is Subset of NAT by A3, XBOOLE_1:1; :: thesis: verum