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_of (TOP-REAL 2) | ((L~ f) ` ) 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_of (TOP-REAL 2) | ((L~ f) ` ) by CONNSP_1:def 6;
A5: B2 is Subset of ((L~ f) ` ) by Lm1;
then A6: Down (RightComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by A3, A4, XBOOLE_1:28;
A7: B1 is Subset of ((L~ f) ` ) by Lm1;
then Down (LeftComp f),((L~ f) ` ) is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) 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