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