let f be non constant standard special_circular_sequence; :: thesis: ( LeftComp f is open & RightComp f is open )
A1: (L~ f) ` is open by TOPS_1:29;
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
hence LeftComp f is open by A1, Th18; :: thesis: RightComp f is open
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
hence RightComp f is open by A1, Th18; :: thesis: verum