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
LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( C is connected & i <= j implies LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) )
assume that
A1: C is connected and
A2: i <= j ; :: thesis: LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j))
A3: (Cage (C,j)) /. 1 = N-min (L~ (Cage (C,j))) by A1, JORDAN9:32;
( i < j or i = j ) by A2, XXREAL_0:1;
then A4: ( E-bound (L~ (Cage (C,i))) > E-bound (L~ (Cage (C,j))) or E-bound (L~ (Cage (C,i))) = E-bound (L~ (Cage (C,j))) ) by A1, JORDAN1A:67;
set p = |[((E-bound (L~ (Cage (C,i)))) + 1),0]|;
A5: LeftComp (Cage (C,i)) misses RightComp (Cage (C,i)) by GOBRD14:14;
A6: |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 = (E-bound (L~ (Cage (C,i)))) + 1 ;
|[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 > E-bound (L~ (Cage (C,i))) by XREAL_1:29;
then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 > E-bound (L~ (Cage (C,j))) by A4, XXREAL_0:2;
then A7: |[((E-bound (L~ (Cage (C,i)))) + 1),0]| in LeftComp (Cage (C,j)) by A3, JORDAN2C:111;
(Cage (C,i)) /. 1 = N-min (L~ (Cage (C,i))) by A1, JORDAN9:32;
then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| in LeftComp (Cage (C,i)) by A6, JORDAN2C:111, XREAL_1:29;
then A8: LeftComp (Cage (C,i)) meets LeftComp (Cage (C,j)) by A7, XBOOLE_0:3;
( Cl (RightComp (Cage (C,i))) = (RightComp (Cage (C,i))) \/ (L~ (Cage (C,i))) & L~ (Cage (C,i)) misses LeftComp (Cage (C,i)) ) by GOBRD14:21, SPRECT_3:26;
then Cl (RightComp (Cage (C,i))) misses LeftComp (Cage (C,i)) by A5, XBOOLE_1:70;
then L~ (Cage (C,j)) misses LeftComp (Cage (C,i)) by A1, A2, Th46, XBOOLE_1:63;
then ( LeftComp (Cage (C,j)) is_a_component_of (L~ (Cage (C,j))) ` & LeftComp (Cage (C,i)) c= (L~ (Cage (C,j))) ` ) by GOBOARD9:def 1, SUBSET_1:23;
hence LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by A8, GOBOARD9:4; :: thesis: verum