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