let n be Element of NAT ; :: thesis: ( n > 1 & n <> 4 & not n is prime implies ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) )
assume A1: ( n > 1 & n <> 4 ) ; :: thesis: ( n is prime or ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) )
assume A2: not n is prime ; :: thesis: ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )

per cases ( n <= 1 or ex k being natural number st
( k divides n & not k = 1 & not k = n ) ) by A2, INT_2:def 5;

suppose n <= 1 ; :: thesis: ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )

hence ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) by A1; :: thesis: verum

end;

suppose ex k being natural number st
( k divides n & not k = 1 & not k = n ) ; :: thesis: ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n )

then consider k being natural number such that
A3: k divides n and
A4: ( k <> 1 & k <> n ) ;
consider m being Nat such that
A5: n = k * m by A3, NAT_D:def 3;
A6: m <> 1 by A4, A5;
A7: m <> n by A1, A4, A5, XCMPLX_1:7;
A8: m divides n by A5, NAT_D:def 3;
A9: k is non empty Element of NAT by A1, A3, INT_2:3, ORDINAL1:def 13;
A10: m is non empty Element of NAT by A1, A5, ORDINAL1:def 13;
( k <> 2 or m <> 2 ) by A1, A5;
hence ex k being non empty Element of NAT st
( k <> 1 & k <> 2 & k <> n & k divides n ) by A3, A4, A6, A7, A8, A9, A10; :: thesis: verum

end;

end;