theorem Th8: :: BINARI_2:8

for m being non zero Nat holds Intval ((Bin1 m) ^ <*FALSE*>) = 1