for n being Nat holds 0* n in BOOLEAN *