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

( 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