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 that
A1: C is connected and
A2: i <= j ; :: thesis: RightComp (Cage C,j) c= RightComp (Cage C,i)
A3: Cl (LeftComp (Cage C,i)) c= Cl (LeftComp (Cage C,j)) by A1, A2, 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 A3, SUBSET_1:31; :: thesis: verum