theorem Th44: :: SPRECT_1:44

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