let n be non zero Nat; :: thesis: NatDivisors n c= Seg n
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NatDivisors n or x in Seg n )
assume x in NatDivisors n ; :: thesis: x in Seg n
then consider k being Nat such that
A1: x = k and
A2: ( k <> 0 & k divides n ) ;
( 1 <= k & k <= n ) by A2, NAT_1:14, NAT_D:7;
hence x in Seg n by A1, FINSEQ_1:1; :: thesis: verum