let i, j be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
RightComp (Cage C,j) c= RightComp (Cage C,i)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( C is connected & i <= j implies RightComp (Cage C,j) c= RightComp (Cage C,i) )
assume ( C is connected & i <= j ) ; :: thesis: RightComp (Cage C,j) c= RightComp (Cage C,i)
then A1: Cl (LeftComp (Cage C,i)) c= Cl (LeftComp (Cage C,j)) by Th55, PRE_TOPC:49;
( (Cl (LeftComp (Cage C,i))) ` = RightComp (Cage C,i) & (Cl (LeftComp (Cage C,j))) ` = RightComp (Cage C,j) ) by Th50;
hence RightComp (Cage C,j) c= RightComp (Cage C,i) by A1, SUBSET_1:31; :: thesis: verum