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