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

per cases ( n <= 1 or ex k being Nat st
( k divides n & not k = 1 & not k = n ) ) by A3, INT_2:def 4;

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

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

end;

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

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

end;

end;