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
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:34;
( 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:88;
set p = |[((E-bound (L~ (Cage (C,i)))) + 1),0]|;
A5: LeftComp (Cage (C,i)) misses RightComp (Cage (C,i)) by GOBRD14:24;
A6: |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 = (E-bound (L~ (Cage (C,i)))) + 1 by EUCLID:56;
then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 > E-bound (L~ (Cage (C,i))) by XREAL_1:31;
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:119;
(Cage (C,i)) /. 1 = N-min (L~ (Cage (C,i))) by A1, JORDAN9:34;
then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| in LeftComp (Cage (C,i)) by A6, JORDAN2C:119, XREAL_1:31;
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:31, SPRECT_3:43;
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, Th54, 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:43;
hence LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by A8, GOBOARD9:6; :: thesis: verum