diff --git a/specifications/MultiCarElevator/Elevator.tla b/specifications/MultiCarElevator/Elevator.tla
index 62389aa5..233264e8 100644
--- a/specifications/MultiCarElevator/Elevator.tla
+++ b/specifications/MultiCarElevator/Elevator.tla
@@ -16,6 +16,8 @@ CONSTANTS   Person,     \* The set of all people using the elevator system
             Elevator,   \* The set of all elevators
             FloorCount  \* The number of floors serviced by the elevator system
 
+ASSUME FloorCountIsPositive == FloorCount \in (Nat \ {0})
+
 VARIABLES   PersonState,            \* The state of each person
             ActiveElevatorCalls,    \* The set of all active elevator calls
             ElevatorState           \* The state of each elevator