ex n being natural number st
( n divides 4 & n <> 1 & n <> 4 )

proof

take 2 ; :: thesis: ( 2 divides 4 & 2 <> 1 & 2 <> 4 )
4 = 2 * 2 ;
hence ( 2 divides 4 & 2 <> 1 & 2 <> 4 ) by INT_1:def 9; :: thesis: verum

end;

hence not 4 is prime by Def5; :: thesis: verum