for f being non constant standard special_circular_sequence holds
( (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is a_union_of_components of (TOP-REAL 2) | ((L~ f) `) & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f )