:: deftheorem defines N-min PSCOMP_1:def 21 :
for X being Subset of (TOP-REAL 2) holds N-min X = |[(lower_bound (proj1 | (N-most X))),(N-bound X)]|;