let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C meets RightComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: C meets RightComp (Cage (C,n))
( N-min C in C & N-min C in RightComp (Cage (C,n)) ) by Th8, SPRECT_1:11;
then C /\ (RightComp (Cage (C,n))) <> {} by XBOOLE_0:def 4;
hence C meets RightComp (Cage (C,n)) ; :: thesis: verum