theorem :: NAT_4:59

for n being Nat st n < 5 & n is prime & not n = 2 holds
n = 3 by Lm2;