theorem Th5: :: BINARI_2:5

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