defpred S₁[ Nat] means ex p being Nat st
( p is prime & p divides $1 );
A1: for k being Nat st k >= 2 & ( for n being Nat st n >= 2 & n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( k >= 2 & ( for n being Nat st n >= 2 & n < k holds
S₁[n] ) implies S₁[k] )
assume A2: k >= 2 ; :: thesis: ( ex n being Nat st
( n >= 2 & n < k & not S₁[n] ) or S₁[k] )
assume A3: for n being Nat st n >= 2 & n < k holds
ex p being Nat st
( p is prime & p divides n ) ; :: thesis: S₁[k]
A4: (k + 1) - 1 > (1 + 1) - 1 by A2, NAT_1:13;
( not k is prime implies ex p being Element of NAT st
( p is prime & p divides k ) )

proof

assume not k is prime ; :: thesis: ex p being Element of NAT st
( p is prime & p divides k )
then consider m being Nat such that
A5: m divides k and
A6: m <> 1 and
A7: m <> k by A4;
m <> 0 by A5, A7;
then m > 0 ;
then m >= 0 + 1 by NAT_1:13;
then m > 1 by A6, XXREAL_0:1;
then A8: m >= 1 + 1 by NAT_1:13;
m <= k by A2, A5, Th27;
then m < k by A7, XXREAL_0:1;
then consider p1 being Nat such that
A9: ( p1 is prime & p1 divides m ) by A3, A8;
reconsider p1 = p1 as Element of NAT by ORDINAL1:def 12;
take p1 ; :: thesis: ( p1 is prime & p1 divides k )
thus ( p1 is prime & p1 divides k ) by A5, A9, Lm2; :: thesis: verum

end;

hence S₁[k] ; :: thesis: verum

end;

A10: for k being Nat st k >= 2 holds
S₁[k] from NAT_1:sch 9(A1);
let n be Nat; :: thesis: ( n >= 2 implies ex p being Element of NAT st
( p is prime & p divides n ) )
assume n >= 2 ; :: thesis: ex p being Element of NAT st
( p is prime & p divides n )
then consider p being Nat such that
A11: ( p is prime & p divides n ) by A10;
reconsider p = p as Element of NAT by ORDINAL1:def 12;
take p ; :: thesis: ( p is prime & p divides n )
thus ( p is prime & p divides n ) by A11; :: thesis: verum