theorem :: NUMBER19:20

for n being natural odd number st n > 1 holds
( n is prime & n + 2 is prime iff ( not n divides (n -' 1) ! & not n + 2 divides (n -' 1) ! ) ) by Th18, Th19;