let f be V8() standard special_circular_sequence; :: thesis: for A1, A2 being Subset of (TOP-REAL 2) st (L~ f) ` = A1 \/ A2 & A1 misses A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st C1 = A1 & C2 = A2 holds

( C1 is a_component & C2 is a_component ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds

( A1 = LeftComp f & A2 = RightComp f )

let A1, A2 be Subset of (TOP-REAL 2); :: thesis: ( (L~ f) ` = A1 \/ A2 & A1 misses A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st C1 = A1 & C2 = A2 holds

( C1 is a_component & C2 is a_component ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) implies ( A1 = LeftComp f & A2 = RightComp f ) )

assume that

A1: (L~ f) ` = A1 \/ A2 and

A2: A1 /\ A2 = {} and

A3: for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st C1 = A1 & C2 = A2 holds

( C1 is a_component & C2 is a_component ) ; :: according to XBOOLE_0:def 7 :: thesis: ( ( A1 = RightComp f & A2 = LeftComp f ) or ( A1 = LeftComp f & A2 = RightComp f ) )

the carrier of ((TOP-REAL 2) | ((L~ f) `)) = (L~ f) ` by PRE_TOPC:8;

then reconsider C1 = A1, C2 = A2 as Subset of ((TOP-REAL 2) | ((L~ f) `)) by A1, XBOOLE_1:7;

C1 = A1 ;

then C2 is a_component by A3;

then A4: ( C2 = RightComp f or C2 = LeftComp f ) by Th12;

C2 = A2 ;

then C1 is a_component by A3;

then A5: ( C1 = RightComp f or C1 = LeftComp f ) by Th12;

assume ( not ( A1 = RightComp f & A2 = LeftComp f ) & not ( A1 = LeftComp f & A2 = RightComp f ) ) ; :: thesis: contradiction

hence contradiction by A2, A5, A4; :: thesis: verum

( C1 is a_component & C2 is a_component ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds

( A1 = LeftComp f & A2 = RightComp f )

let A1, A2 be Subset of (TOP-REAL 2); :: thesis: ( (L~ f) ` = A1 \/ A2 & A1 misses A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st C1 = A1 & C2 = A2 holds

( C1 is a_component & C2 is a_component ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) implies ( A1 = LeftComp f & A2 = RightComp f ) )

assume that

A1: (L~ f) ` = A1 \/ A2 and

A2: A1 /\ A2 = {} and

A3: for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st C1 = A1 & C2 = A2 holds

( C1 is a_component & C2 is a_component ) ; :: according to XBOOLE_0:def 7 :: thesis: ( ( A1 = RightComp f & A2 = LeftComp f ) or ( A1 = LeftComp f & A2 = RightComp f ) )

the carrier of ((TOP-REAL 2) | ((L~ f) `)) = (L~ f) ` by PRE_TOPC:8;

then reconsider C1 = A1, C2 = A2 as Subset of ((TOP-REAL 2) | ((L~ f) `)) by A1, XBOOLE_1:7;

C1 = A1 ;

then C2 is a_component by A3;

then A4: ( C2 = RightComp f or C2 = LeftComp f ) by Th12;

C2 = A2 ;

then C1 is a_component by A3;

then A5: ( C1 = RightComp f or C1 = LeftComp f ) by Th12;

assume ( not ( A1 = RightComp f & A2 = LeftComp f ) & not ( A1 = LeftComp f & A2 = RightComp f ) ) ; :: thesis: contradiction

hence contradiction by A2, A5, A4; :: thesis: verum