theorem :: JORDAN5D:27

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 = N-bound (L~ h) & q in L~ h ) } holds
upper_bound X = upper_bound (proj1 | (N-most (L~ h))) by Th15;