let f be V8() standard special_circular_sequence; :: thesis: for P being Subset of (() | ((L~ f) `)) holds
( not P is a_component or P = RightComp f or P = LeftComp f )

let P be Subset of (() | ((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 <> {} (() | ((L~ f) `)) by ;
then consider a being Point of (() | ((L~ f) `)) such that
A3: a in P by SUBSET_1:4;
( the carrier of (() | ((L~ f) `)) = (L~ f) ` & (L~ f) ` = () \/ () ) by ;
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 (() | ((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 (() | ((L~ f) `)) such that
A6: R = RightComp f and
A7: R is a_component by CONNSP_1:def 6;
P misses R by ;
then P meets LeftComp f by ;
hence P = LeftComp f by ; :: thesis: verum