definitions of the continuant part of at some time property and at is at all time subproperty looks circular

[kbserm]

b continuant part of c at some time =Def for some time t (b exists at t and c exists at t and b continuant part of c at t & t is a temporal region & b and c are continuants)

b continuant part of c at all times =Def for all times t, (b exists at t, implies b continuant part of c at t & t is a temporal region & b and c are continuants)

[johnbeve]

@kbserm The idea here was to provide first-order logic definitions connecting binary relations (which would provide the foundation for OWL) to ternary relations (which cannot be expressed in OWL). The difference lies in the fact that the left-hand-side does not quantify over time explicitly, while the right-hand-side explicitly quantifies over time.