theorem Th4: :: BINARI_3:4

for n being Nat holds 0* n in BOOLEAN *