(Forall (?Physdim ?Spatdim) (Abelian-Group (Dyad-Of-Dimensions ?Physdim ?Spatdim) + (The-Zero-Dyad-Of-Type ?Spatdim ?Physdim))) (<- (Dyad-Of-Dimensions ?Physim ?Spatdim) (If (And (Physical-Dimension ?Physim) (Positive-Integer ?Spatdim)) (Kappa (?Vq) (And (Dyad ?Vq) (= (Spatial.Dimension ?Vq) ?Spatdim) (= (Quantity.Dimension ?Vq) ?Physim)))))