let n be non zero Nat; :: thesis: PrimeDivisors n c= Seg n
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors n or x in Seg n )
assume x in PrimeDivisors n ; :: thesis: x in Seg n
then consider k being Prime such that
A1: x = k and
A2: k divides n ;
A3: 1 <= k by INT_2:def 4;
k <= n by A2, INT_2:27;
hence x in Seg n by A1, A3; :: thesis: verum