let j, i be 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 Th47, PRE_TOPC:19;
( (Cl (LeftComp (Cage (C,i)))) ` = RightComp (Cage (C,i)) & (Cl (LeftComp (Cage (C,j)))) ` = RightComp (Cage (C,j)) ) by Th42;
hence RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) by A1, SUBSET_1:12; :: thesis: verum