theorem Th43: :: SPRECT_1:43

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