:: deftheorem defines W-bound PSCOMP_1:def 7 :
for X being Subset of (TOP-REAL 2) holds W-bound X = lower_bound (proj1 | X);