let n be Element of 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 set ; :: 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)) = {} by XBOOLE_0:def 7;
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)) = {} by XBOOLE_0:def 7;
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:28; :: thesis: verum