for g being FinSequence of (TOP-REAL 2)
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds
lower_bound X = lower_bound (proj1 | (L~ g)) by Th17;