let n, k be Nat; :: thesis: ( n divides k & 1 < n implies ex p being Element of NAT st
( p divides k & p <= n & p is prime ) )
assume A1: n divides k ; :: thesis: ( not 1 < n or ex p being Element of NAT st
( p divides k & p <= n & p is prime ) )
assume A2: 1 < n ; :: thesis: ex p being Element of NAT st
( p divides k & p <= n & p is prime )
then 1 + 1 < n + 1 by XREAL_1:6;
then 2 <= n by NAT_1:13;
then consider p being Element of NAT such that
A3: p is prime and
A4: p divides n by INT_2:31;
take p ; :: thesis: ( p divides k & p <= n & p is prime )
thus p divides k by A1, A4, NAT_D:4; :: thesis: ( p <= n & p is prime )
thus p <= n by A2, A4, NAT_D:7; :: thesis: p is prime
thus p is prime by A3; :: thesis: verum