set X = seq (m,n);

seq (m,n) c= NAT

seq (m,n) c= NAT

proof

hence
seq (m,n) is Subset of NAT
; :: thesis: verum
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;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