let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses LeftComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: C misses LeftComp (Cage (C,n))
set f = Cage (C,n);
assume A1: C meets LeftComp (Cage (C,n)) ; :: thesis: contradiction
RightComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) ` by GOBOARD9:def 2;
then A2: ex R being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st
( R = RightComp (Cage (C,n)) & R is a_component ) by CONNSP_1:def 6;
C misses L~ (Cage (C,n)) by Th5;
then A3: C /\ (L~ (Cage (C,n))) = {} ;
C c= the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `))
proof
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) )
assume A4: c in C ; :: thesis: c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `))
then not c in L~ (Cage (C,n)) by A3, XBOOLE_0:def 4;
then c in (L~ (Cage (C,n))) ` by A4, SUBSET_1:29;
hence c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) by PRE_TOPC:8; :: thesis: verum
end;
then reconsider C1 = C as Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) ;
LeftComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) ` by GOBOARD9:def 1;
then A5: ex L being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st
( L = LeftComp (Cage (C,n)) & L is a_component ) by CONNSP_1:def 6;
( C meets RightComp (Cage (C,n)) & C1 is connected ) by Th9, CONNSP_1:23;
hence contradiction by A1, A5, A2, JORDAN2C:92, SPRECT_4:6; :: thesis: verum