( ∀ [V__Q2,V__U,V__I1,V__I2,V__Q1]
((s__instance(V__Q2,s__PhysicalQuantity)s__and__ms__instance(V__U,s__UnitOfMeasure)s__and__ms__instance(V__I1,s__RealNumber)s__and__ms__instance(V__I2,s__RealNumber)s__and__ms__instance(V__Q1,s__PhysicalQuantity))
s__=>((s__instance(s__greaterThan__m,s__RelationExtendedToQuantities)s__and__m(V__Q1s__equal__ms__MeasureFn(V__I1,V__U))
s__and__m(V__Q2s__equal__ms__MeasureFn(V__I2,V__U))
s__and__ms__greaterThan(V__I1,V__I2))
s__=>s__greaterThan(V__Q1,V__Q2)))
)
( ∀ [V__Q2,V__U,V__I1,V__I2,V__Q1]
((s__instance(V__Q2,s__PhysicalQuantity)s__and__ms__instance(V__U,s__UnitOfMeasure)s__and__ms__instance(V__I1,s__RealNumber)s__and__ms__instance(V__I2,s__RealNumber)s__and__ms__instance(V__Q1,s__PhysicalQuantity))
s__=>((s__instance(s__lessThan__m,s__RelationExtendedToQuantities)s__and__m(V__Q1s__equal__ms__MeasureFn(V__I1,V__U))
s__and__m(V__Q2s__equal__ms__MeasureFn(V__I2,V__U))
s__and__ms__lessThan(V__I1,V__I2))
s__=>s__lessThan(V__Q1,V__Q2)))
)
( ∀ [V__Q2,V__U,V__I1,V__I2,V__Q1]
((s__instance(V__Q2,s__PhysicalQuantity)s__and__ms__instance(V__U,s__UnitOfMeasure)s__and__ms__instance(V__I1,s__RealNumber)s__and__ms__instance(V__I2,s__RealNumber)s__and__ms__instance(V__Q1,s__PhysicalQuantity))
s__=>((s__instance(s__greaterThanOrEqualTo__m,s__RelationExtendedToQuantities)s__and__m(V__Q1s__equal__ms__MeasureFn(V__I1,V__U))
s__and__m(V__Q2s__equal__ms__MeasureFn(V__I2,V__U))
s__and__ms__greaterThanOrEqualTo(V__I1,V__I2))
s__=>s__greaterThanOrEqualTo(V__Q1,V__Q2)))
)
( ∀ [V__Q2,V__U,V__I1,V__I2,V__Q1]
((s__instance(V__Q2,s__PhysicalQuantity)s__and__ms__instance(V__U,s__UnitOfMeasure)s__and__ms__instance(V__I1,s__RealNumber)s__and__ms__instance(V__I2,s__RealNumber)s__and__ms__instance(V__Q1,s__PhysicalQuantity))
s__=>((s__instance(s__lessThanOrEqualTo__m,s__RelationExtendedToQuantities)s__and__m(V__Q1s__equal__ms__MeasureFn(V__I1,V__U))
s__and__m(V__Q2s__equal__ms__MeasureFn(V__I2,V__U))
s__and__ms__lessThanOrEqualTo(V__I1,V__I2))
s__=>s__lessThanOrEqualTo(V__Q1,V__Q2)))
)

Merge.kif 65976603 

( ∀ [V__NUMBER1,V__NUMBER2]
((s__instance(s__greaterThanOrEqualTo__m,s__RelationExtendedToQuantities)s__and__ms__instance(s__greaterThanOrEqualTo__m,s__BinaryPredicate)s__and__ms__instance(V__NUMBER1,s__RealNumber)s__and__ms__instance(V__NUMBER2,s__RealNumber)s__and__ms__greaterThanOrEqualTo(V__NUMBER1,V__NUMBER2))
s__=>(s__forall__m[V__UNIT]
(s__instance(V__UNIT,s__UnitOfMeasure)s__=>s__greaterThanOrEqualTo(s__MeasureFn(V__NUMBER1,V__UNIT)
,s__MeasureFn(V__NUMBER2,V__UNIT)))))
)
( ∀ [V__NUMBER1,V__NUMBER2]
((s__instance(s__greaterThan__m,s__RelationExtendedToQuantities)s__and__ms__instance(s__greaterThan__m,s__BinaryPredicate)s__and__ms__instance(V__NUMBER1,s__RealNumber)s__and__ms__instance(V__NUMBER2,s__RealNumber)s__and__ms__greaterThan(V__NUMBER1,V__NUMBER2))
s__=>(s__forall__m[V__UNIT]
(s__instance(V__UNIT,s__UnitOfMeasure)s__=>s__greaterThan(s__MeasureFn(V__NUMBER1,V__UNIT)
,s__MeasureFn(V__NUMBER2,V__UNIT)))))
)
( ∀ [V__NUMBER1,V__NUMBER2]
((s__instance(s__lessThan__m,s__RelationExtendedToQuantities)s__and__ms__instance(s__lessThan__m,s__BinaryPredicate)s__and__ms__instance(V__NUMBER1,s__RealNumber)s__and__ms__instance(V__NUMBER2,s__RealNumber)s__and__ms__lessThan(V__NUMBER1,V__NUMBER2))
s__=>(s__forall__m[V__UNIT]
(s__instance(V__UNIT,s__UnitOfMeasure)s__=>s__lessThan(s__MeasureFn(V__NUMBER1,V__UNIT)
,s__MeasureFn(V__NUMBER2,V__UNIT)))))
)
( ∀ [V__NUMBER1,V__NUMBER2]
((s__instance(s__lessThanOrEqualTo__m,s__RelationExtendedToQuantities)s__and__ms__instance(s__lessThanOrEqualTo__m,s__BinaryPredicate)s__and__ms__instance(V__NUMBER1,s__RealNumber)s__and__ms__instance(V__NUMBER2,s__RealNumber)s__and__ms__lessThanOrEqualTo(V__NUMBER1,V__NUMBER2))
s__=>(s__forall__m[V__UNIT]
(s__instance(V__UNIT,s__UnitOfMeasure)s__=>s__lessThanOrEqualTo(s__MeasureFn(V__NUMBER1,V__UNIT)
,s__MeasureFn(V__NUMBER2,V__UNIT)))))
)

Merge.kif 65856595 
