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

now :: thesis: for e being object st e in { i where i is Nat : ( m <= i & i <= n ) } holds
e in {0} \/ (Seg n)

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

now :: thesis: e in {0} \/ (Seg n)

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;
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 Nat : ( m <= i & i <= n ) } c= {0} \/ (Seg n) ;
hence nat_interval (m,n) is finite ; :: thesis: verum