ex n being Nat 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 ) ; :: thesis: verum

end;

hence not 4 is prime ; :: thesis: verum