let f be non 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_of (TOP-REAL 2) | ((L~ f) ` ) & C2 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) ) ) & 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_of (TOP-REAL 2) | ((L~ f) ` ) & C2 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) ) ) & 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_of (TOP-REAL 2) | ((L~ f) ` ) & C2 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) ) ; :: 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:29;
then reconsider C1 = A1, C2 = A2 as Subset of ((TOP-REAL 2) | ((L~ f) ` )) by A1, XBOOLE_1:7;
A4: ( C1 = A1 & C2 = A2 ) ;
then A5: C1 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by A3;
C2 is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by A3, A4;
then A6: ( ( C1 = RightComp f or C1 = LeftComp f ) & ( C2 = RightComp f or C2 = LeftComp f ) ) by A5, Th22;
assume ( not ( A1 = RightComp f & A2 = LeftComp f ) & not ( A1 = LeftComp f & A2 = RightComp f ) ) ; :: thesis: contradiction
hence contradiction by A2, A6; :: thesis: verum