:: deftheorem defines E-bound PSCOMP_1:def 9 :
for X being Subset of (TOP-REAL 2) holds E-bound X = upper_bound (proj1 | X);