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)
A1: N-min C in C by SPRECT_1:13;
N-min C in RightComp (Cage C,n) by Th8;
then C /\ (RightComp (Cage C,n)) <> {} by A1, XBOOLE_0:def 4;
hence C meets RightComp (Cage C,n) by XBOOLE_0:def 7; :: thesis: verum