let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= RightComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: C c= RightComp (Cage (C,n))
set f = Cage (C,n);
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in RightComp (Cage (C,n)) )
assume A1: c in C ; :: thesis: c in RightComp (Cage (C,n))
C misses L~ (Cage (C,n)) by Th5;
then C /\ (L~ (Cage (C,n))) = {} ;
then A2: not c in L~ (Cage (C,n)) by A1, XBOOLE_0:def 4;
C misses LeftComp (Cage (C,n)) by Th10;
then C /\ (LeftComp (Cage (C,n))) = {} ;
then not c in LeftComp (Cage (C,n)) by A1, XBOOLE_0:def 4;
hence c in RightComp (Cage (C,n)) by A1, A2, GOBRD14:18; :: thesis: verum