theorem :: NUMBER16:20
( ( for n being non zero Nat st n < 6 holds
value ((<%1%> ^ (n --> 3)),10) is prime ) & not value ((<%1%> ^ (8 --> 3)),10) is prime & { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime } is infinite )