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