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:8;
then 2 <= n by NAT_1:13;
then consider p being Element of NAT such that
A3: ( p is prime & p divides n ) by INT_2:48;
take p ; :: thesis: ( p divides k & p <= n & p is prime )
thus p divides k by A1, A3, NAT_D:4; :: thesis: ( p <= n & p is prime )
thus p <= n by A2, A3, NAT_D:7; :: thesis: p is prime
thus p is prime by A3; :: thesis: verum