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