for f being rectangular special_circular_sequence
for p being Point of (TOP-REAL 2) st ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) holds
p in LeftComp f