let n be Element of 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:13;
then C /\ (RightComp (Cage C,n)) <> {} by XBOOLE_0:def 4;
hence C meets RightComp (Cage C,n) by XBOOLE_0:def 7; :: thesis: verum