theorem Th15: :: NUMBER04:15

for n being even Nat st n divides (2 |^ n) + 2 & n - 1 divides (2 |^ n) + 1 holds
for n1 being Nat st n1 = (2 |^ n) + 2 holds
( n1 - 1 divides (2 |^ n1) + 1 & n1 divides (2 |^ n1) + 2 )