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