Base Template PropertyRangeMagnitudeRestrictionOfClass

PropertyRangeMagnitudeRestrictionOfClass is a template for stating which range of values of a property can apply to a class of individuals.
PropertyRangeMagnitudeRestrictionOfClass(a, b, c, d, e) means that a is a class of individuals, b is a property relation, c is a scale, and d and e are real numbers, and that every b property of an a has a value in the d to e range, measured on the c scale.

Roles:
1 hasClass ClassOfIndividual
2 hasRestrictedProperty ClassOfIndirectProperty
3 hasScale Scale
4 valUpperBound ExpressReal
5 valLowerBound ExpressReal

Axiom:

PropertyRangeMagnitudeRestrictionOfClass(x1, x2, x3, x4, x5) <-> 
ClassOfIndividual(x1)& 
ClassOfIndirectProperty(x2)& 
Scale(x3)& 
ExpressReal(x4)& 
ExpressReal(x5)& 
exists u(PropertyRangeRestrictionOfClass(x1, x2, u)& 
exists y1 exists y2(IdentificationByNumber(x4, y1)& 
IdentificationByNumber(x5, y2)& 
LowerUpperMagnitudeOfPropertyRange(u, x3, y1, y2))) .