let m, n be Element of NAT ; :: thesis: ( 1 <= m implies nat_interval (m,n) c= Seg n )
assume A1: 1 <= m ; :: thesis: nat_interval (m,n) c= Seg n

now

let e be set ; :: thesis: ( e in nat_interval (m,n) implies e in Seg n )
assume e in nat_interval (m,n) ; :: thesis: e in Seg n
then consider i being Element of NAT such that
A2: e = i and
A3: m <= i and
A4: i <= n ;
1 <= i by A1, A3, XXREAL_0:2;
hence e in Seg n by A2, A4, FINSEQ_1:1; :: thesis: verum

end;

hence nat_interval (m,n) c= Seg n by TARSKI:def 3; :: thesis: verum