theorem Th6: :: BINARI_2:6

for n, i being Nat st i in Seg n & i <> 1 holds
(Bin1 n) /. i = FALSE