:: deftheorem defines S-bound PSCOMP_1:def 10 :
for X being Subset of (TOP-REAL 2) holds S-bound X = lower_bound (proj2 | X);