:: deftheorem defines N-bound PSCOMP_1:def 8 :
for X being Subset of (TOP-REAL 2) holds N-bound X = upper_bound (proj2 | X);