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