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 & B1 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) ) by CONNSP_1:def 6;
A2: B1 is Subset of ((L~ f) ` ) by Lm1;
then A3: Down (LeftComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by A1, XBOOLE_1:28;
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
A4: ( B2 = RightComp f & B2 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) ) by CONNSP_1:def 6;
A5: B2 is Subset of ((L~ f) ` ) by Lm1;
then Down (RightComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by A4, 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, A2, A3, A4, A5, GOBRD11:3, XBOOLE_1:28; :: thesis: verum