theorem :: JORDAN5D:24

for h being non constant standard special_circular_sequence
for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : ( q `2 = S-bound (L~ h) & q in L~ h ) } holds
lower_bound X = lower_bound (proj1 | (S-most (L~ h))) by Th16;