theorem :: ORDINAL5:20

for n being Nat holds
( 0 |^|^ (2 * n) = 1 & 0 |^|^ ((2 * n) + 1) = 0 )