theorem Th11: :: BINARI_3:11

for n being non zero Nat holds Absval (Bin1 n) = 1