let l be natural number ; :: thesis: ( l >= 2 implies ex p being Element of NAT st
( p is prime & p divides l ) )
assume A1: l >= 2 ; :: thesis: ex p being Element of NAT st
( p is prime & p divides l )
defpred S₁[ Nat] means ex p being natural number st
( p is prime & p divides $1 );
A2: 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 A3: k >= 2 ; :: thesis: ( ex n being Nat st
( n >= 2 & n < k & not S₁[n] ) or S₁[k] )
then A4: (k + 1) - 1 > (1 + 1) - 1 by NAT_1:13;
assume A5: for n being Nat st n >= 2 & n < k holds
ex p being natural number st
( p is prime & p divides n ) ; :: thesis: S₁[k]
( 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 natural number such that
A6: ( m divides k & m <> 1 & m <> k ) by A4, Def5;
( m >= 2 & m < k )

proof

thus m >= 2 :: thesis: m < k

proof

m <> 0 by A6, Th3;
then m > 0 by NAT_1:3;
then m >= 0 + 1 by NAT_1:13;
then m > 1 by A6, XXREAL_0:1;
then m >= 1 + 1 by NAT_1:13;
hence m >= 2 ; :: thesis: verum

end;

k > 0 by A3, XXREAL_0:2;
then m <= k by A6, Th43;
hence m < k by A6, XXREAL_0:1; :: thesis: verum

end;

then consider p1 being natural number such that
A7: ( p1 is prime & p1 divides m ) by A5;
reconsider p1 = p1 as Element of NAT by ORDINAL1:def 13;
take p1 ; :: thesis: ( p1 is prime & p1 divides k )
thus ( p1 is prime & p1 divides k ) by A6, A7, Lm2; :: thesis: verum

end;

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

end;

for k being Nat st k >= 2 holds
S₁[k] from NAT_1:sch 9(A2);
then consider p being natural number such that
A8: ( p is prime & p divides l ) by A1;
reconsider p = p as Element of NAT by ORDINAL1:def 13;
take p ; :: thesis: ( p is prime & p divides l )
thus ( p is prime & p divides l ) by A8; :: thesis: verum