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:8;
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:19; :: 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