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
X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h)))