theorem Th46: :: SPRECT_1:46

for S being Subset of (TOP-REAL 2) holds E-bound S = upper_bound (proj1 .: S)