let f be non constant standard special_circular_sequence; :: thesis: ( (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is a_union_of_components of (TOP-REAL 2) | ((L~ f) `) & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f )
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A1: B1 = LeftComp f and
A2: B1 is a_component by CONNSP_1:def 6;
RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
then consider B2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A3: B2 = RightComp f and
A4: B2 is a_component by CONNSP_1:def 6;
A5: B2 is Subset of ((L~ f) `) by Lm1;
then A6: Down ((RightComp f),((L~ f) `)) is a_component by A3, A4, XBOOLE_1:28;
A7: B1 is Subset of ((L~ f) `) by Lm1;
then Down ((LeftComp f),((L~ f) `)) is a_component by A1, A2, XBOOLE_1:28;
hence ( (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is a_union_of_components of (TOP-REAL 2) | ((L~ f) `) & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by A1, A7, A3, A5, A6, GOBRD11:3, XBOOLE_1:28; :: thesis: verum