let m, n be 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 :: thesis: for e being object st e in nat_interval (m,n) holds
e in Seg n

let e be object ; :: 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 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; :: thesis: verum

end;

hence nat_interval (m,n) c= Seg n ; :: thesis: verum