let r, s be Real; :: thesis: for F being Subset-Family of (Closed-Interval-TSpace (r,s)) st [.r,s.] in F & r <= s holds
( rng <*[.r,s.]*> c= F & union (rng <*[.r,s.]*>) = [.r,s.] & ( for n being Nat st 1 <= n holds
( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) ) ) )
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis: ( [.r,s.] in F & r <= s implies ( rng <*[.r,s.]*> c= F & union (rng <*[.r,s.]*>) = [.r,s.] & ( for n being Nat st 1 <= n holds
( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) ) ) ) )
assume that
A1: [.r,s.] in F and
A2: r <= s ; :: thesis: ( rng <*[.r,s.]*> c= F & union (rng <*[.r,s.]*>) = [.r,s.] & ( for n being Nat st 1 <= n holds
( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) ) ) )
set f = <*[.r,s.]*>;
A3: rng <*[.r,s.]*> = {[.r,s.]} by FINSEQ_1:38;
thus rng <*[.r,s.]*> c= F by A1, A3, TARSKI:def 1; :: thesis: ( union (rng <*[.r,s.]*>) = [.r,s.] & ( for n being Nat st 1 <= n holds
( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) ) ) )
thus union (rng <*[.r,s.]*>) = [.r,s.] by A3, ZFMISC_1:25; :: thesis: for n being Nat st 1 <= n holds
( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) )
let n be Nat; :: thesis: ( 1 <= n implies ( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) ) )
assume A4: 1 <= n ; :: thesis: ( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) )
hereby :: thesis: ( ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) )
assume n <= len <*[.r,s.]*> ; :: thesis: not <*[.r,s.]*> /. n is empty
then n <= 1 by FINSEQ_1:39;
then n = 1 by A4, XXREAL_0:1;
then <*[.r,s.]*> /. n = [.r,s.] by FINSEQ_4:16;
hence not <*[.r,s.]*> /. n is empty by A2, XXREAL_1:1; :: thesis: verum
end;
hereby :: thesis: ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) )
assume n + 1 <= len <*[.r,s.]*> ; :: thesis: ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) )
then n + 1 <= 0 + 1 by FINSEQ_1:39;
hence ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) by A4, XREAL_1:6; :: thesis: verum
end;
assume n + 2 <= len <*[.r,s.]*> ; :: thesis: upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2))
then (n + 1) + 1 <= 0 + 1 by FINSEQ_1:39;
hence upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) by XREAL_1:6; :: thesis: verum