DISCRETE-TIME-RANGE-CLASS denotes a time range whose start time and end time are measured by a time-range-unit.
(<=> (Discrete-Time-Range-Class ?Class) (And (Class ?Class) (Value-Cardinality ?Class Time-Range-Unit 1) (Forall (?I) (=> (Instance-Of ?I ?Class) (And (Measured-By (Time-Range.Start-Time ?I) (Time-Range-Unit ?Class)) (Measured-By (Time-Range.End-Time ?I) (Time-Range-Unit ?Class)))))))
(Forall (?I) (=> (Instance-Of ?I ?Class) (And (Measured-By (Time-Range.Start-Time ?I) (Time-Range-Unit ?Class)) (Measured-By (Time-Range.End-Time ?I) (Time-Range-Unit ?Class))))) (Class ?Class)
(<=> (Discrete-Time-Range-Class ?Class) (And (Class ?Class) (Value-Cardinality ?Class Time-Range-Unit 1) (Forall (?I) (=> (Instance-Of ?I ?Class) (And (Measured-By (Time-Range.Start-Time ?I) (Time-Range-Unit ?Class)) (Measured-By (Time-Range.End-Time ?I) (Time-Range-Unit ?Class))))))) (=> (Time-Range-Unit $X $Y) (Discrete-Time-Range-Class $X)) (<=> (Unit-Time-Range-Class ?Class) (And (Discrete-Time-Range-Class ?Class) (Forall (?I) (=> (Instance-Of ?I ?Class) (= (Time-Range.Duration ?I) (Time-Range-Unit ?Class))))))