theorem Th45: :: SPRECT_1:45

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