now :: thesis: for p being Nat st p > 1 & ( for n being Element of NAT holds
( not 1 < n or not n * n <= p or not n is prime or not n divides p ) ) holds
p is prime

let p be Nat; :: thesis: ( p > 1 & ( for n being Element of NAT holds
( not 1 < n or not n * n <= p or not n is prime or not n divides p ) ) implies p is prime )
assume A1: p > 1 ; :: thesis: ( ( for n being Element of NAT holds
( not 1 < n or not n * n <= p or not n is prime or not n divides p ) ) implies p is prime )
assume for n being Element of NAT holds
( not 1 < n or not n * n <= p or not n is prime or not n divides p ) ; :: thesis: p is prime
then for n being Element of NAT holds
( not n divides p or not 1 < n or not n * n <= p or not n is prime ) ;
hence p is prime by A1, Lm1; :: thesis: verum

end;

hence for p being Nat holds
( p is prime iff ( p > 1 & ( for n being Element of NAT st 1 < n & n * n <= p & n is prime holds
not n divides p ) ) ) by Lm1; :: thesis: verum