for f being rectangular special_circular_sequence holds L~ f = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }