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