let n be Nat; :: thesis: ( n > 1 implies ex p being Prime st
( p divides n & ( for q being Prime st q divides n holds
q <= p ) ) )
assume A1: n > 1 ; :: thesis: ex p being Prime st
( p divides n & ( for q being Prime st q divides n holds
q <= p ) )
defpred S₁[ Nat] means ( $1 is prime & $1 divides n );
A2: for k being Nat st S₁[k] holds
k <= n by A1, NAT_D:7;
n >= 1 + 1 by A1, NAT_1:13;
then ex p being Element of NAT st
( p is prime & p divides n ) by INT_2:31;
then A3: ex k being Nat st S₁[k] ;
consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A2, A3);
reconsider k = k as Prime by A4;
take k ; :: thesis: ( k divides n & ( for q being Prime st q divides n holds
q <= k ) )
thus ( k divides n & ( for q being Prime st q divides n holds
q <= k ) ) by A4; :: thesis: verum