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