let r, s be Real; :: thesis: for n being Nat
for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len G holds
[.(G . n),(G . (n + 1)).] c= C . n
let n be Nat; :: thesis: for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len G holds
[.(G . n),(G . (n + 1)).] c= C . n
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis: for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len G holds
[.(G . n),(G . (n + 1)).] c= C . n
let C be IntervalCover of F; :: thesis: for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len G holds
[.(G . n),(G . (n + 1)).] c= C . n
let G be IntervalCoverPts of C; :: thesis: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len G implies [.(G . n),(G . (n + 1)).] c= C . n )
set L = Closed-Interval-TSpace (r,s);
assume that
A1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open ) and
A2: F is connected and
A3: r <= s and
A4: 1 <= n and
A5: n < len G ; :: thesis: [.(G . n),(G . (n + 1)).] c= C . n
A6: len G = (len C) + 1 by A1, A2, A3, Def3;
then A7: n <= len C by A5, NAT_1:13;
then A8: C /. n = C . n by A4, FINSEQ_4:15;
n in dom C by A4, A7, FINSEQ_3:25;
then A9: C . n in rng C by FUNCT_1:def 3;
rng C c= F by A1, A2, A3, Def2;
then C /. n in F by A8, A9;
then C /. n is connected Subset of (Closed-Interval-TSpace (r,s)) by A2;
then A10: C /. n is interval by Th43;
A11: not C /. n is empty by A1, A2, A3, A4, A7, Def2;
A12: n + 1 <= len G by A5, NAT_1:13;
0 + 1 <= n + 1 by XREAL_1:6;
then A13: n + 1 in dom G by A12, FINSEQ_3:25;
A14: n in dom G by A4, A5, FINSEQ_3:25;
A15: n + 0 < n + 1 by XREAL_1:6;
per cases ( r = s or r < s ) by A3, XXREAL_0:1;
suppose r = s ; :: thesis: [.(G . n),(G . (n + 1)).] c= C . n
then C = <*[.r,r.]*> by A1, A2, Th50;
then A16: len C = 1 by FINSEQ_1:40;
then G = <*r,s*> by A1, A2, A3, Th61;
then A17: ( G . 1 = r & G . 2 = s ) by FINSEQ_1:44;
( n = 1 & C = <*[.r,s.]*> ) by A1, A2, A3, A4, A7, A16, Th52, XXREAL_0:1;
hence [.(G . n),(G . (n + 1)).] c= C . n by A17, FINSEQ_1:40; :: thesis: verum
end;
suppose r < s ; :: thesis: [.(G . n),(G . (n + 1)).] c= C . n
then G is increasing by A1, A2, Th65;
then A18: G . n < G . (n + 1) by A14, A13, A15;
A19: 2 <= len G by A1, A2, A3, Th60;
per cases ( ( n = 1 & len G = 2 ) or ( n = 1 & 1 + 1 < len G ) or ( 1 < n & len G = n + 1 ) or ( 1 < n & n + 1 < len G ) ) by A4, A12, A19, XXREAL_0:1;
suppose that A20: n = 1 and
A21: len G = 2 ; :: thesis: [.(G . n),(G . (n + 1)).] c= C . n
G = <*r,s*> by A1, A2, A3, A6, A21, Th61;
then A22: ( G . 1 = r & G . 2 = s ) by FINSEQ_1:44;
C = <*[.r,s.]*> by A1, A2, A3, A6, A21, Th52;
hence [.(G . n),(G . (n + 1)).] c= C . n by A20, A22, FINSEQ_1:40; :: thesis: verum
end;
suppose that A23: n = 1 and
A24: 1 + 1 < len G ; :: thesis: [.(G . n),(G . (n + 1)).] c= C . n
G . (1 + 1) in ].(lower_bound (C /. (1 + 1))),(upper_bound (C /. 1)).[ by A1, A2, A3, A24, Def3;
then A25: lower_bound (C /. (1 + 1)) < G . 2 by XXREAL_1:4;
1 + 1 <= len C by A6, A24, NAT_1:13;
then lower_bound (C /. 1) <= lower_bound (C /. (1 + 1)) by A1, A2, A3, Def2;
then A26: lower_bound (C /. n) < G . (n + 1) by A23, A25, XXREAL_0:2;
A27: ( G . 1 = r & r in C /. 1 ) by A1, A2, A3, Def3, Th57;
G . (n + 1) < upper_bound (C /. n) by A1, A2, A3, A23, A24, Th62;
then G . (n + 1) in C . n by A8, A10, A11, A26, Th30;
hence [.(G . n),(G . (n + 1)).] c= C . n by A8, A10, A23, A27; :: thesis: verum
end;
suppose that A28: 1 < n and
A29: len G = n + 1 ; :: thesis: [.(G . n),(G . (n + 1)).] c= C . n
1 - 1 < n - 1 by A28, XREAL_1:9;
then A30: ( 0 + 1 <= n - 1 & n - 1 is Element of NAT ) by INT_1:3, INT_1:7;
then G . ((n - 1) + 1) in ].(lower_bound (C /. ((n - 1) + 1))),(upper_bound (C /. (n - 1))).[ by A1, A2, A3, A15, A29, Def3;
then A31: G . n < upper_bound (C /. (n - 1)) by XXREAL_1:4;
upper_bound (C /. (n - 1)) <= upper_bound (C /. ((n - 1) + 1)) by A1, A2, A3, A6, A29, A30, Def2;
then A32: G . n < upper_bound (C /. n) by A31, XXREAL_0:2;
G . (len G) = s by A1, A2, A3, Def3;
then A33: G . (n + 1) in C . n by A1, A2, A3, A6, A8, A29, Th59;
lower_bound (C /. n) < G . n by A1, A2, A3, A6, A28, A29, Th63;
then G . n in C . n by A8, A10, A11, A32, Th30;
hence [.(G . n),(G . (n + 1)).] c= C . n by A8, A10, A33; :: thesis: verum
end;
suppose that A34: 1 < n and
A35: n + 1 < len G ; :: thesis: [.(G . n),(G . (n + 1)).] c= C . n
A36: G . (n + 1) < upper_bound (C /. n) by A1, A2, A3, A4, A35, Th62;
n <= len C by A5, A6, NAT_1:13;
then A37: lower_bound (C /. n) < G . n by A1, A2, A3, A34, Th63;
then lower_bound (C /. n) < G . (n + 1) by A18, XXREAL_0:2;
then A38: G . (n + 1) in C . n by A8, A10, A11, A36, Th30;
G . n < upper_bound (C /. n) by A18, A36, XXREAL_0:2;
then G . n in C . n by A8, A10, A11, A37, Th30;
hence [.(G . n),(G . (n + 1)).] c= C . n by A8, A10, A38; :: thesis: verum
end;
end;
end;
end;