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