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)
set p = |[((E-bound (L~ (Cage C,i))) + 1),0 ]|;
A3: |[((E-bound (L~ (Cage C,i))) + 1),0 ]| `1 = (E-bound (L~ (Cage C,i))) + 1 by EUCLID:56;
then A4: |[((E-bound (L~ (Cage C,i))) + 1),0 ]| `1 > E-bound (L~ (Cage C,i)) by XREAL_1:31;
(Cage C,i) /. 1 = N-min (L~ (Cage C,i)) by A1, JORDAN9:34;
then A5: |[((E-bound (L~ (Cage C,i))) + 1),0 ]| in LeftComp (Cage C,i) by A3, JORDAN2C:119, XREAL_1:31;
( i < j or i = j ) by A2, XXREAL_0:1;
then ( 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;
then A6: |[((E-bound (L~ (Cage C,i))) + 1),0 ]| `1 > E-bound (L~ (Cage C,j)) by A4, XXREAL_0:2;
(Cage C,j) /. 1 = N-min (L~ (Cage C,j)) by A1, JORDAN9:34;
then |[((E-bound (L~ (Cage C,i))) + 1),0 ]| in LeftComp (Cage C,j) by A6, JORDAN2C:119;
then A7: LeftComp (Cage C,i) meets LeftComp (Cage C,j) by A5, XBOOLE_0:3;
A8: LeftComp (Cage C,j) is_a_component_of (L~ (Cage C,j)) ` by GOBOARD9:def 1;
A9: Cl (RightComp (Cage C,i)) = (RightComp (Cage C,i)) \/ (L~ (Cage C,i)) by GOBRD14:31;
A10: L~ (Cage C,i) misses LeftComp (Cage C,i) by SPRECT_3:43;
LeftComp (Cage C,i) misses RightComp (Cage C,i) by GOBRD14:24;
then Cl (RightComp (Cage C,i)) misses LeftComp (Cage C,i) by A9, A10, XBOOLE_1:70;
then L~ (Cage C,j) misses LeftComp (Cage C,i) by A1, A2, Th54, XBOOLE_1:63;
then LeftComp (Cage C,i) c= (L~ (Cage C,j)) ` by SUBSET_1:43;
hence LeftComp (Cage C,i) c= LeftComp (Cage C,j) by A7, A8, GOBOARD9:6; :: thesis: verum