let f be constant 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