theorem :: JORDAN5D:22

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