let f be non constant standard special_circular_sequence; :: thesis: ( Cl (Down (RightComp f),((L~ f) ` )) is connected & Down (RightComp f),((L~ f) ` ) = RightComp f & Down (RightComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ f) ` )) such that
A1: ( B1 = RightComp f & B1 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) ) by CONNSP_1:def 6;
A2: the carrier of ((TOP-REAL 2) | ((L~ f) ` )) = (L~ f) ` by PRE_TOPC:29;
then Down (RightComp f),((L~ f) ` ) = RightComp f by A1, XBOOLE_1:28;
then Down (RightComp f),((L~ f) ` ) is connected by A1, CONNSP_1:def 5;
hence Cl (Down (RightComp f),((L~ f) ` )) is connected by CONNSP_1:20; :: thesis: ( Down (RightComp f),((L~ f) ` ) = RightComp f & Down (RightComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) )
thus ( Down (RightComp f),((L~ f) ` ) = RightComp f & Down (RightComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) ) by A1, A2, XBOOLE_1:28; :: thesis: verum