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

let p be Nat; :: thesis: ( not p is prime & not p <= 1 implies ex n being Element of NAT st
( n divides p & 1 < n & n < p ) )
assume that
A1: not p is prime and
A2: not p <= 1 ; :: thesis: ex n being Element of NAT st
( n divides p & 1 < n & n < p )
consider n being Nat such that
A3: n divides p and
A4: ( n <> 1 & n <> p ) by A1, A2, INT_2:def 4;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n = n; :: thesis: ( n divides p & 1 < n & n < p )
thus n divides p by A3; :: thesis: ( 1 < n & n < p )
thus ( 1 < n & n < p ) by A2, A3, A4, Th7; :: thesis: verum

end;

hence for p being Nat holds
( ( p <= 1 or ex n being Element of NAT st
( n divides p & 1 < n & n < p ) ) iff not p is prime ) by INT_2:def 4; :: thesis: verum