(=>
(and
(instance ?AREA GeographicArea)
(geographicSubregion
(ElevationHighPointFn ?AREA) ?AREA)
(elevation
(ElevationHighPointFn ?AREA)
(MeasureFn ?ELEV1 ?UNIT)))
(not
(exists (?OTHER ?ELEV2)
(and
(geographicSubregion ?OTHER ?AREA)
(not
(equal ?OTHER
(ElevationHighPointFn ?AREA)))
(elevation ?OTHER
(MeasureFn ?ELEV2 ?UNIT))
(greaterThan ?ELEV2 ?ELEV1))))) |
Geography.kif 3415-3426 |
If X is an instance of geographic area, the elevation high point of X is a geographic subregion of X, and Y Z(s) is an elevation of the elevation high point of X, then there don't exist W and V such that W is a geographic subregion of X and equal W and the elevation high point of X and V Z(s) is an elevation of W and V is greater than Y |