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