let f be non constant standard special_circular_sequence; :: thesis: for P being Subset of ((TOP-REAL 2) | ((L~ f) ` )) holds
( not P is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) or P = RightComp f or P = LeftComp f )
let P be Subset of ((TOP-REAL 2) | ((L~ f) ` )); :: thesis: ( not P is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) or P = RightComp f or P = LeftComp f )
assume that
A1: P is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) and
A2: P <> RightComp f ; :: thesis: P = LeftComp f
P <> {} ((TOP-REAL 2) | ((L~ f) ` )) by A1, CONNSP_1:34;
then consider a being Point of ((TOP-REAL 2) | ((L~ f) ` )) such that
A3: a in P by SUBSET_1:10;
( the carrier of ((TOP-REAL 2) | ((L~ f) ` )) = (L~ f) ` & (L~ f) ` = (LeftComp f) \/ (RightComp f) ) by GOBRD12:11, PRE_TOPC:29;
then A4: ( a in LeftComp f or a in RightComp f ) by XBOOLE_0:def 3;
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
then A5: ex L being Subset of ((TOP-REAL 2) | ((L~ f) ` )) st
( L = LeftComp f & L 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 R being Subset of ((TOP-REAL 2) | ((L~ f) ` )) such that
A6: R = RightComp f and
A7: R is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by CONNSP_1:def 6;
P misses R by A1, A2, A6, A7, CONNSP_1:37;
then P meets LeftComp f by A6, A3, A4, XBOOLE_0:3;
hence P = LeftComp f by A1, A5, CONNSP_1:37; :: thesis: verum