let f be V22() standard special_circular_sequence; :: thesis: ( LeftComp f is open & RightComp f is open )
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
hence LeftComp f is open by Th8; :: thesis: RightComp f is open
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
hence RightComp f is open by Th8; :: thesis: verum