now

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 A1: ( not p is prime & not p <= 1 ) ; :: thesis: ex n being Element of NAT st
( n divides p & 1 < n & n < p )
then consider n being Nat such that
A2: ( n divides p & n <> 1 & n <> p ) by INT_2:def 5;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
take n = n; :: thesis: ( n divides p & 1 < n & n < p )
thus n divides p by A2; :: thesis: ( 1 < n & n < p )
thus ( 1 < n & n < p ) by A1, A2, 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 5; :: thesis: verum