set X = seq m,n;
seq m,n c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in seq m,n or x in NAT )
assume x in seq m,n ; :: thesis: x in NAT
then ex i being Element of NAT st
( x = i & 1 + m <= i & i <= n + m ) ;
hence x in NAT ; :: thesis: verum

end;

hence seq m,n is Subset of NAT ; :: thesis: verum