set X = seq (m,n);
seq (m,n) c= NAT
proof
let x be object ; :: 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