(subclass PositiveRealNumber NonnegativeRealNumber) | Merge.kif 1932-1932 | NumeroRealePositivo è una sottoclasse di NumeroRealeNonNegativo |
(subclass PositiveInteger PositiveRealNumber) | Merge.kif 1995-1995 | NumeroInteroPositivo è una sottoclasse di NumeroRealePositivo |