rcomp_3.miz

begin

 registration

 let X be non empty set;

 cluster ( [#] X) -> non empty;

 coherence ;

 end

 registration

 cluster -> real-membered for SubSpace of RealSpace ;

 coherence

 proof

 let T be SubSpace of RealSpace ;

 the carrier of T is Subset of RealSpace by TOPMETR:def 1;

 hence the carrier of T is real-membered;

 end;

 end

 theorem :: RCOMP_3:1



 Th1: for X be non empty bounded_below real-membered set, Y be closed Subset of REAL st X c= Y holds ( lower_bound X) in Y

 proof

 let X be non empty bounded_below real-membered set;

 let Y be closed Subset of REAL ;

 assume

 A1: X c= Y;

 reconsider X as non empty bounded_below Subset of REAL by MEMBERED: 3;



 A2: ( lower_bound X) = ( lower_bound ( Cl X)) & ( lower_bound ( Cl X)) in ( Cl X) by RCOMP_1: 13, TOPREAL6: 68;

 ( Cl X) c= Y by A1, MEASURE6: 57;

 hence thesis by A2;

 end;

 theorem :: RCOMP_3:2



 Th2: for X be non empty bounded_above real-membered set, Y be closed Subset of REAL st X c= Y holds ( upper_bound X) in Y

 proof

 let X be non empty bounded_above real-membered set;

 let Y be closed Subset of REAL ;

 assume

 A1: X c= Y;

 reconsider X as non empty bounded_above Subset of REAL by MEMBERED: 3;



 A2: ( upper_bound X) = ( upper_bound ( Cl X)) & ( upper_bound ( Cl X)) in ( Cl X) by RCOMP_1: 12, TOPREAL6: 69;

 ( Cl X) c= Y by A1, MEASURE6: 57;

 hence thesis by A2;

 end;

 theorem :: RCOMP_3:3



 Th3: for X,Y be Subset of REAL holds ( Cl (X \/ Y)) = (( Cl X) \/ ( Cl Y))

 proof

 let X,Y be Subset of REAL ;

 reconsider A = X, B = Y as Subset of R^1 by TOPMETR: 17;



 thus ( Cl (X \/ Y)) = ( Cl (A \/ B)) by JORDAN5A: 24

 .= (( Cl A) \/ ( Cl B)) by PRE_TOPC: 20

 .= (( Cl X) \/ ( Cl B)) by JORDAN5A: 24

 .= (( Cl X) \/ ( Cl Y)) by JORDAN5A: 24;

 end;

 begin

 reserve a,b,r,s for Real;

 registration

 let r be Real, s be ExtReal;

 cluster [.r, s.[ -> bounded_below;

 coherence

 proof

 take r;

 let x be ExtReal;

 thus thesis by XXREAL_1: 3;

 end;

 cluster ].s, r.] -> bounded_above;

 coherence

 proof

 take r;

 let x be ExtReal;

 thus thesis by XXREAL_1: 2;

 end;

 end

 registration

 let r, s;

 cluster [.r, s.[ -> real-bounded;

 coherence

 proof

 [.r, s.[ is bounded_above

 proof

 take s;

 let x be ExtReal;

 thus thesis by XXREAL_1: 3;

 end;

 hence thesis;

 end;

 cluster ].r, s.] -> real-bounded;

 coherence

 proof

 ].r, s.] is bounded_below

 proof

 take r;

 let x be ExtReal;

 thus thesis by XXREAL_1: 2;

 end;

 hence thesis;

 end;

 cluster ].r, s.[ -> real-bounded;

 coherence

 proof



 A1: ].r, s.[ is bounded_above

 proof

 take s;

 let x be ExtReal;

 thus thesis by XXREAL_1: 4;

 end;

 ].r, s.[ is bounded_below

 proof

 take r;

 let x be ExtReal;

 thus thesis by XXREAL_1: 4;

 end;

 hence thesis by A1;

 end;

 end

 registration

 cluster open real-bounded interval non empty for Subset of REAL ;

 existence

 proof

 take ]. 0 , 1.[;

 thus thesis;

 end;

 end

 theorem :: RCOMP_3:4



 Th4: r < s implies ( lower_bound [.r, s.[) = r

 proof

 set X = [.r, s.[;

 assume

 A1: r < s;



 A2: for a st a in X holds r <= a by XXREAL_1: 3;



 A3: ((r + s) / 2) < s by A1, XREAL_1: 226;



 A4: r < ((r + s) / 2) by A1, XREAL_1: 226;



 A5: for b st 0 = (r + b);

 per cases ;

 suppose (r + b) > s;

 then

 A8: ((r + s) / 2) < (r + b) by A3, XXREAL_0: 2;

 ((r + s) / 2) in X by A4, A3, XXREAL_1: 3;

 hence thesis by A7, A8;

 end;

 suppose

 A9: (r + b) <= s;



 A10: r < (r + b) by A6, XREAL_1: 29;

 then ((r + (r + b)) / 2) < (r + b) by XREAL_1: 226;

 then

 A11: ((r + (r + b)) / 2) < s by A9, XXREAL_0: 2;

 r < ((r + (r + b)) / 2) by A10, XREAL_1: 226;

 then ((r + (r + b)) / 2) in X by A11, XXREAL_1: 3;

 hence thesis by A7, A10, XREAL_1: 226;

 end;

 end;

 X is non empty by A1, XXREAL_1: 3;

 hence thesis by A2, A5, SEQ_4:def 2;

 end;

 theorem :: RCOMP_3:5



 Th5: r < s implies ( upper_bound [.r, s.[) = s

 proof

 set X = [.r, s.[;

 assume

 A1: r < s;



 A2: for a st a in X holds a <= s by XXREAL_1: 3;



 A3: r < ((r + s) / 2) by A1, XREAL_1: 226;



 A4: ((r + s) / 2) < s by A1, XREAL_1: 226;



 A5: for b st 0 < b holds ex a st a in X & (s - b) < a

 proof

 let b such that

 A6: 0 (s - b) by A3, XXREAL_0: 2;

 ((r + s) / 2) in X by A3, A4, XXREAL_1: 3;

 hence thesis by A7, A8;

 end;

 suppose

 A9: (s - b) > r;



 A10: (s - b) < (s - 0 ) by A6, XREAL_1: 15;

 then (s - b) < ((s + (s - b)) / 2) by XREAL_1: 226;

 then

 A11: r < ((s + (s - b)) / 2) by A9, XXREAL_0: 2;

 ((s + (s - b)) / 2) < s by A10, XREAL_1: 226;

 then ((s + (s - b)) / 2) in X by A11, XXREAL_1: 3;

 hence thesis by A7, A10, XREAL_1: 226;

 end;

 end;

 X is non empty by A1, XXREAL_1: 3;

 hence thesis by A2, A5, SEQ_4:def 1;

 end;

 theorem :: RCOMP_3:6



 Th6: r < s implies ( lower_bound ].r, s.]) = r

 proof

 set X = ].r, s.];

 assume

 A1: r < s;



 A2: for a st a in X holds r <= a by XXREAL_1: 2;



 A3: ((r + s) / 2) < s by A1, XREAL_1: 226;



 A4: r < ((r + s) / 2) by A1, XREAL_1: 226;



 A5: for b st 0 = (r + b);

 per cases ;

 suppose (r + b) > s;

 then

 A8: ((r + s) / 2) < (r + b) by A3, XXREAL_0: 2;

 ((r + s) / 2) in X by A4, A3, XXREAL_1: 2;

 hence thesis by A7, A8;

 end;

 suppose

 A9: (r + b) <= s;



 A10: r < (r + b) by A6, XREAL_1: 29;

 then ((r + (r + b)) / 2) < (r + b) by XREAL_1: 226;

 then

 A11: ((r + (r + b)) / 2) < s by A9, XXREAL_0: 2;

 r < ((r + (r + b)) / 2) by A10, XREAL_1: 226;

 then ((r + (r + b)) / 2) in X by A11, XXREAL_1: 2;

 hence thesis by A7, A10, XREAL_1: 226;

 end;

 end;

 X is non empty by A1, XXREAL_1: 2;

 hence thesis by A2, A5, SEQ_4:def 2;

 end;

 theorem :: RCOMP_3:7



 Th7: r < s implies ( upper_bound ].r, s.]) = s

 proof

 set X = ].r, s.];

 assume

 A1: r < s;



 A2: for a st a in X holds a <= s by XXREAL_1: 2;



 A3: r < ((r + s) / 2) by A1, XREAL_1: 226;



 A4: ((r + s) / 2) < s by A1, XREAL_1: 226;



 A5: for b st 0 < b holds ex a st a in X & (s - b) < a

 proof

 let b such that

 A6: 0 (s - b) by A3, XXREAL_0: 2;

 ((r + s) / 2) in X by A3, A4, XXREAL_1: 2;

 hence thesis by A7, A8;

 end;

 suppose

 A9: (s - b) > r;



 A10: (s - b) < (s - 0 ) by A6, XREAL_1: 15;

 then (s - b) < ((s + (s - b)) / 2) by XREAL_1: 226;

 then

 A11: r < ((s + (s - b)) / 2) by A9, XXREAL_0: 2;

 ((s + (s - b)) / 2) < s by A10, XREAL_1: 226;

 then ((s + (s - b)) / 2) in X by A11, XXREAL_1: 2;

 hence thesis by A7, A10, XREAL_1: 226;

 end;

 end;

 X is non empty by A1, XXREAL_1: 2;

 hence thesis by A2, A5, SEQ_4:def 1;

 end;

 begin

 theorem :: RCOMP_3:8



 Th8: a <= b implies ( [.a, b.] /\ (( left_closed_halfline a) \/ ( right_closed_halfline b))) = {a, b}

 proof

 set A = ( left_closed_halfline a);

 set B = ( right_closed_halfline b);

 assume a <= b;

 then

 A1: a in [.a, b.] & b in [.a, b.] by XXREAL_1: 1;

 thus ( [.a, b.] /\ (A \/ B)) c= {a, b}

 proof

 let x be object;

 assume

 A2: x in ( [.a, b.] /\ (A \/ B));

 then

 reconsider x as Real;

 x in (A \/ B) by A2, XBOOLE_0:def 4;

 then x in A or x in B by XBOOLE_0:def 3;

 then

 A3: x <= a or x >= b by XXREAL_1: 234, XXREAL_1: 236;

 x in [.a, b.] by A2, XBOOLE_0:def 4;

 then a <= x & x <= b by XXREAL_1: 1;

 then x = a or x = b by A3, XXREAL_0: 1;

 hence thesis by TARSKI:def 2;

 end;

 let x be object;

 a in A by XXREAL_1: 234;

 then

 A4: a in (A \/ B) by XBOOLE_0:def 3;

 b in B by XXREAL_1: 236;

 then

 A5: b in (A \/ B) by XBOOLE_0:def 3;

 assume x in {a, b};

 then x = a or x = b by TARSKI:def 2;

 hence thesis by A1, A4, A5, XBOOLE_0:def 4;

 end;

 Lm1:

 now

 let a;

 assume ( left_open_halfline a) is bounded_below;

 then

 consider b such that

 A1: b is LowerBound of ( left_open_halfline a);



 A2: for r st r in ( left_open_halfline a) holds b <= r by A1, XXREAL_2:def 2;



 A3: (a - 1) < (a - 0 ) by XREAL_1: 15;

 then (a - 1) in ( left_open_halfline a) by XXREAL_1: 233;

 then (b - 1) < ((a - 1) - 0 ) by A2, XREAL_1: 15;

 then (b - 1) < a by A3, XXREAL_0: 2;

 then (b - 1) in ( left_open_halfline a) by XXREAL_1: 233;

 then (b - 0 ) <= (b - 1) by A1, XXREAL_2:def 2;

 hence contradiction by XREAL_1: 15;

 end;

 Lm2:

 now

 let a;

 assume ( right_open_halfline a) is bounded_above;

 then

 consider b such that

 A1: b is UpperBound of ( right_open_halfline a);



 A2: (a + 0 ) < (a + 1) by XREAL_1: 6;

 then (a + 1) in ( right_open_halfline a) by XXREAL_1: 235;

 then (a + 1) <= b by A1, XXREAL_2:def 1;

 then ((a + 1) + 0 ) <= (b + 1) by XREAL_1: 7;

 then a < (b + 1) by A2, XXREAL_0: 2;

 then (b + 1) in ( right_open_halfline a) by XXREAL_1: 235;

 then (b + 1) <= (b + 0 ) by A1, XXREAL_2:def 1;

 hence contradiction by XREAL_1: 6;

 end;

 registration

 let a;

 cluster ( left_closed_halfline a) -> non bounded_below bounded_above interval;

 coherence

 proof

 set A = ( left_closed_halfline a);

 not ( left_open_halfline a) is bounded_below by Lm1;

 hence A is non bounded_below by XXREAL_1: 21, XXREAL_2: 44;

 thus A is bounded_above;

 let r,s be ExtReal;

 assume

 A1: r in A & s in A;

 then

 reconsider rr = r, ss = s as Real;



 A2: s <= a by A1, XXREAL_1: 234;

 let x be object;

 assume

 A3: x in [.r, s.];

 then x in [.rr, ss.];

 then

 reconsider x as Real;

 x <= s by A3, XXREAL_1: 1;

 then x <= a by A2, XXREAL_0: 2;

 hence thesis by XXREAL_1: 234;

 end;

 cluster ( left_open_halfline a) -> non bounded_below bounded_above interval;

 coherence

 proof

 set A = ( left_open_halfline a);

 thus A is non bounded_below by Lm1;

 thus A is bounded_above

 proof

 take a;

 let x be ExtReal;

 thus thesis by XXREAL_1: 233;

 end;

 let r,s be ExtReal;

 assume

 A4: r in A;

 assume

 A5: s in A;

 then

 A6: s < a by XXREAL_1: 233;

 reconsider rr = r, ss = s as Real by A4, A5;

 let x be object;

 assume

 A7: x in [.r, s.];

 then x in [.rr, ss.];

 then

 reconsider x as Real;

 x <= s by A7, XXREAL_1: 1;

 then x < a by A6, XXREAL_0: 2;

 hence thesis by XXREAL_1: 233;

 end;

 cluster ( right_closed_halfline a) -> bounded_below non bounded_above interval;

 coherence

 proof

 set A = ( right_closed_halfline a);

 thus A is bounded_below;

 not ( right_open_halfline a) is bounded_above by Lm2;

 hence A is non bounded_above by XXREAL_1: 22, XXREAL_2: 43;

 let r,s be ExtReal;

 assume

 A8: r in A;

 then

 A9: a <= r by XXREAL_1: 236;

 assume s in A;

 then

 reconsider rr = r, ss = s as Real by A8;

 let x be object;

 assume

 A10: x in [.r, s.];

 then x in [.rr, ss.];

 then

 reconsider x as Real;

 r <= x by A10, XXREAL_1: 1;

 then a <= x by A9, XXREAL_0: 2;

 hence thesis by XXREAL_1: 236;

 end;

 cluster ( right_open_halfline a) -> bounded_below non bounded_above interval;

 coherence

 proof

 set A = ( right_open_halfline a);

 thus A is bounded_below

 proof

 take a;

 let x be ExtReal;

 thus thesis by XXREAL_1: 235;

 end;

 thus A is non bounded_above by Lm2;

 let r,s be ExtReal;

 assume

 A11: r in A;

 then

 A12: a < r by XXREAL_1: 235;

 assume s in A;

 then

 reconsider rr = r, ss = s as Real by A11;

 let x be object;

 assume

 A13: x in [.r, s.];

 then x in [.rr, ss.];

 then

 reconsider x as Real;

 r <= x by A13, XXREAL_1: 1;

 then a < x by A12, XXREAL_0: 2;

 hence thesis by XXREAL_1: 235;

 end;

 end

 theorem :: RCOMP_3:9



 Th9: ( upper_bound ( left_closed_halfline a)) = a

 proof

 set X = ( left_closed_halfline a);



 A1: for s st 0 < s holds ex r st r in X & (a - s) < r

 proof

 let s;

 assume 0 < s;

 then

 A2: (a - s) < (a - 0 ) by XREAL_1: 15;

 take a;

 thus a in X by XXREAL_1: 234;

 thus thesis by A2;

 end;

 for r st r in X holds r <= a by XXREAL_1: 234;

 hence thesis by A1, SEQ_4:def 1;

 end;

 theorem :: RCOMP_3:10



 Th10: ( upper_bound ( left_open_halfline a)) = a

 proof

 set X = ( left_open_halfline a);



 A1: for s st 0 < s holds ex r st r in X & (a - s) < r

 proof

 let s;

 assume 0 < s;

 then

 A2: (a - s) < (a - 0 ) by XREAL_1: 15;

 take (((a - s) + a) / 2);

 (((a - s) + a) / 2) < a by A2, XREAL_1: 226;

 hence thesis by A2, XREAL_1: 226, XXREAL_1: 233;

 end;

 for r st r in X holds r <= a by XXREAL_1: 233;

 hence thesis by A1, SEQ_4:def 1;

 end;

 theorem :: RCOMP_3:11



 Th11: ( lower_bound ( right_closed_halfline a)) = a

 proof

 set X = ( right_closed_halfline a);



 A1: for s st 0 < s holds ex r st r in X & r < (a + s)

 proof

 let s;

 assume 0 < s;

 then

 A2: (a + 0 ) < (a + s) by XREAL_1: 6;

 take a;

 thus a in X by XXREAL_1: 236;

 thus thesis by A2;

 end;

 for r st r in X holds a <= r by XXREAL_1: 236;

 hence thesis by A1, SEQ_4:def 2;

 end;

 theorem :: RCOMP_3:12



 Th12: ( lower_bound ( right_open_halfline a)) = a

 proof

 set X = ( right_open_halfline a);



 A1: for s st 0 < s holds ex r st r in X & r < (a + s)

 proof

 let s;

 assume 0 < s;

 then

 A2: (a + 0 ) < (a + s) by XREAL_1: 6;

 take (((a + a) + s) / 2);

 a < ((a + (a + s)) / 2) by A2, XREAL_1: 226;

 hence thesis by A2, XREAL_1: 226, XXREAL_1: 235;

 end;

 for r st r in X holds a <= r by XXREAL_1: 235;

 hence thesis by A1, SEQ_4:def 2;

 end;

 begin

 registration

 cluster ( [#] REAL ) -> interval non bounded_below non bounded_above;

 coherence ;

 end

 theorem :: RCOMP_3:13



 Th13: for X be real-bounded interval Subset of REAL st ( lower_bound X) in X & ( upper_bound X) in X holds X = [.( lower_bound X), ( upper_bound X).]

 proof

 let X be real-bounded interval Subset of REAL such that

 A1: ( lower_bound X) in X & ( upper_bound X) in X;

 reconsider X1 = X as non empty real-bounded interval Subset of REAL by A1;

 X1 c= [.( lower_bound X1), ( upper_bound X1).] by XXREAL_2: 69;

 hence X c= [.( lower_bound X), ( upper_bound X).];

 thus thesis by A1, XXREAL_2:def 12;

 end;

 theorem :: RCOMP_3:14



 Th14: for X be real-bounded Subset of REAL st not ( lower_bound X) in X holds X c= ].( lower_bound X), ( upper_bound X).]

 proof

 let X be real-bounded Subset of REAL such that

 A1: not ( lower_bound X) in X;

 let x be object;

 assume

 A2: x in X;

 then

 reconsider x as Real;

 ( lower_bound X) <= x by A2, SEQ_4:def 2;

 then

 A3: ( lower_bound X) < x by A1, A2, XXREAL_0: 1;

 x <= ( upper_bound X) by A2, SEQ_4:def 1;

 hence thesis by A3, XXREAL_1: 2;

 end;

 theorem :: RCOMP_3:15



 Th15: for X be real-bounded interval Subset of REAL st not ( lower_bound X) in X & ( upper_bound X) in X holds X = ].( lower_bound X), ( upper_bound X).]

 proof

 let X be real-bounded interval Subset of REAL such that

 A1: not ( lower_bound X) in X and

 A2: ( upper_bound X) in X;

 thus X c= ].( lower_bound X), ( upper_bound X).] by A1, Th14;

 let x be object;

 assume

 A3: x in ].( lower_bound X), ( upper_bound X).];

 then

 reconsider x as Real;

 ( lower_bound X) < x by A3, XXREAL_1: 2;

 then (( lower_bound X) - ( lower_bound X)) < (x - ( lower_bound X)) by XREAL_1: 14;

 then

 consider r such that

 A4: r in X and

 A5: r < (( lower_bound X) + (x - ( lower_bound X))) by A2, SEQ_4:def 2;

 x <= ( upper_bound X) by A3, XXREAL_1: 2;

 then

 A6: x in [.r, ( upper_bound X).] by A5, XXREAL_1: 1;

 [.r, ( upper_bound X).] c= X by A2, A4, XXREAL_2:def 12;

 hence thesis by A6;

 end;

 theorem :: RCOMP_3:16



 Th16: for X be real-bounded Subset of REAL st not ( upper_bound X) in X holds X c= [.( lower_bound X), ( upper_bound X).[

 proof

 let X be real-bounded Subset of REAL such that

 A1: not ( upper_bound X) in X;

 let x be object;

 assume

 A2: x in X;

 then

 reconsider x as Real;

 x <= ( upper_bound X) by A2, SEQ_4:def 1;

 then

 A3: x < ( upper_bound X) by A1, A2, XXREAL_0: 1;

 ( lower_bound X) <= x by A2, SEQ_4:def 2;

 hence thesis by A3, XXREAL_1: 3;

 end;

 theorem :: RCOMP_3:17



 Th17: for X be real-bounded interval Subset of REAL st ( lower_bound X) in X & not ( upper_bound X) in X holds X = [.( lower_bound X), ( upper_bound X).[

 proof

 let X be real-bounded interval Subset of REAL such that

 A1: ( lower_bound X) in X and

 A2: not ( upper_bound X) in X;

 thus X c= [.( lower_bound X), ( upper_bound X).[ by A2, Th16;

 let x be object;

 assume

 A3: x in [.( lower_bound X), ( upper_bound X).[;

 then

 reconsider x as Real;

 x < ( upper_bound X) by A3, XXREAL_1: 3;

 then (x - x) < (( upper_bound X) - x) by XREAL_1: 14;

 then

 consider r such that

 A4: r in X and

 A5: (( upper_bound X) - (( upper_bound X) - x)) < r by A1, SEQ_4:def 1;

 ( lower_bound X) <= x by A3, XXREAL_1: 3;

 then

 A6: x in [.( lower_bound X), r.] by A5, XXREAL_1: 1;

 [.( lower_bound X), r.] c= X by A1, A4, XXREAL_2:def 12;

 hence thesis by A6;

 end;

 theorem :: RCOMP_3:18



 Th18: for X be real-bounded Subset of REAL st not ( lower_bound X) in X & not ( upper_bound X) in X holds X c= ].( lower_bound X), ( upper_bound X).[

 proof

 let X be real-bounded Subset of REAL such that

 A1: not ( lower_bound X) in X and

 A2: not ( upper_bound X) in X;

 let x be object;

 assume

 A3: x in X;

 then

 reconsider x as Real;

 x <= ( upper_bound X) by A3, SEQ_4:def 1;

 then

 A4: x < ( upper_bound X) by A2, A3, XXREAL_0: 1;

 ( lower_bound X) <= x by A3, SEQ_4:def 2;

 then ( lower_bound X) < x by A1, A3, XXREAL_0: 1;

 hence thesis by A4, XXREAL_1: 4;

 end;

 theorem :: RCOMP_3:19



 Th19: for X be non empty real-bounded interval Subset of REAL st not ( lower_bound X) in X & not ( upper_bound X) in X holds X = ].( lower_bound X), ( upper_bound X).[

 proof

 let X be non empty real-bounded interval Subset of REAL ;

 assume ( not ( lower_bound X) in X) & not ( upper_bound X) in X;

 hence X c= ].( lower_bound X), ( upper_bound X).[ by Th18;

 let x be object;

 assume

 A1: x in ].( lower_bound X), ( upper_bound X).[;

 then

 reconsider x as Real;

 ( lower_bound X) < x by A1, XXREAL_1: 4;

 then (( lower_bound X) - ( lower_bound X)) < (x - ( lower_bound X)) by XREAL_1: 14;

 then

 consider s such that

 A2: s in X & s < (( lower_bound X) + (x - ( lower_bound X))) by SEQ_4:def 2;

 x < ( upper_bound X) by A1, XXREAL_1: 4;

 then (x - x) < (( upper_bound X) - x) by XREAL_1: 14;

 then

 consider r such that

 A3: r in X & (( upper_bound X) - (( upper_bound X) - x)) < r by SEQ_4:def 1;

 [.s, r.] c= X & x in [.s, r.] by A2, A3, XXREAL_1: 1, XXREAL_2:def 12;

 hence thesis;

 end;

 theorem :: RCOMP_3:20



 Th20: for X be Subset of REAL st X is bounded_above holds X c= ( left_closed_halfline ( upper_bound X))

 proof

 let X be Subset of REAL such that

 A1: X is bounded_above;

 let x be object;

 assume

 A2: x in X;

 then

 reconsider x as Real;

 x <= ( upper_bound X) by A1, A2, SEQ_4:def 1;

 hence thesis by XXREAL_1: 234;

 end;

 theorem :: RCOMP_3:21



 Th21: for X be interval Subset of REAL st not X is bounded_below & X is bounded_above & ( upper_bound X) in X holds X = ( left_closed_halfline ( upper_bound X))

 proof

 let X be interval Subset of REAL such that

 A1: not X is bounded_below and

 A2: X is bounded_above and

 A3: ( upper_bound X) in X;

 thus X c= ( left_closed_halfline ( upper_bound X)) by A2, Th20;

 let x be object;

 assume

 A4: x in ( left_closed_halfline ( upper_bound X));

 then

 reconsider x as Real;

 not x is LowerBound of X by A1;

 then

 consider r be ExtReal such that

 A5: r in X and

 A6: x > r by XXREAL_2:def 2;

 reconsider r as Real by A5;

 x <= ( upper_bound X) by A4, XXREAL_1: 234;

 then

 A7: x in [.r, ( upper_bound X).] by A6, XXREAL_1: 1;

 [.r, ( upper_bound X).] c= X by A3, A5, XXREAL_2:def 12;

 hence thesis by A7;

 end;

 theorem :: RCOMP_3:22



 Th22: for X be Subset of REAL st X is bounded_above & not ( upper_bound X) in X holds X c= ( left_open_halfline ( upper_bound X))

 proof

 let X be Subset of REAL such that

 A1: X is bounded_above and

 A2: not ( upper_bound X) in X;

 let x be object;

 assume

 A3: x in X;

 then

 reconsider x as Real;

 x <= ( upper_bound X) by A1, A3, SEQ_4:def 1;

 then x < ( upper_bound X) by A2, A3, XXREAL_0: 1;

 hence thesis by XXREAL_1: 233;

 end;

 theorem :: RCOMP_3:23



 Th23: for X be non empty interval Subset of REAL st not X is bounded_below & X is bounded_above & not ( upper_bound X) in X holds X = ( left_open_halfline ( upper_bound X))

 proof

 let X be non empty interval Subset of REAL such that

 A1: not X is bounded_below and

 A2: X is bounded_above and

 A3: not ( upper_bound X) in X;

 thus X c= ( left_open_halfline ( upper_bound X)) by A2, A3, Th22;

 let x be object;

 assume

 A4: x in ( left_open_halfline ( upper_bound X));

 then

 reconsider x as Real;

 not x is LowerBound of X by A1;

 then

 consider r be ExtReal such that

 A5: r in X & x > r by XXREAL_2:def 2;

 reconsider r as Real by A5;

 x < ( upper_bound X) by A4, XXREAL_1: 233;

 then (x - x) < (( upper_bound X) - x) by XREAL_1: 14;

 then

 consider s such that

 A6: s in X & (( upper_bound X) - (( upper_bound X) - x)) < s by A2, SEQ_4:def 1;

 [.r, s.] c= X & x in [.r, s.] by A5, A6, XXREAL_1: 1, XXREAL_2:def 12;

 hence thesis;

 end;

 theorem :: RCOMP_3:24



 Th24: for X be Subset of REAL st X is bounded_below holds X c= ( right_closed_halfline ( lower_bound X))

 proof

 let X be Subset of REAL such that

 A1: X is bounded_below;

 let x be object;

 assume

 A2: x in X;

 then

 reconsider x as Real;

 ( lower_bound X) <= x by A1, A2, SEQ_4:def 2;

 hence thesis by XXREAL_1: 236;

 end;

 theorem :: RCOMP_3:25



 Th25: for X be interval Subset of REAL st X is bounded_below & not X is bounded_above & ( lower_bound X) in X holds X = ( right_closed_halfline ( lower_bound X))

 proof

 let X be interval Subset of REAL such that

 A1: X is bounded_below and

 A2: not X is bounded_above and

 A3: ( lower_bound X) in X;

 thus X c= ( right_closed_halfline ( lower_bound X)) by A1, Th24;

 let x be object;

 assume

 A4: x in ( right_closed_halfline ( lower_bound X));

 then

 reconsider x as Real;

 not x is UpperBound of X by A2;

 then

 consider r be ExtReal such that

 A5: r in X and

 A6: x < r by XXREAL_2:def 1;

 reconsider r as Real by A5;

 ( lower_bound X) <= x by A4, XXREAL_1: 236;

 then

 A7: x in [.( lower_bound X), r.] by A6, XXREAL_1: 1;

 [.( lower_bound X), r.] c= X by A3, A5, XXREAL_2:def 12;

 hence thesis by A7;

 end;

 theorem :: RCOMP_3:26



 Th26: for X be Subset of REAL st X is bounded_below & not ( lower_bound X) in X holds X c= ( right_open_halfline ( lower_bound X))

 proof

 let X be Subset of REAL such that

 A1: X is bounded_below and

 A2: not ( lower_bound X) in X;

 let x be object;

 assume

 A3: x in X;

 then

 reconsider x as Real;

 ( lower_bound X) <= x by A1, A3, SEQ_4:def 2;

 then ( lower_bound X) < x by A2, A3, XXREAL_0: 1;

 hence thesis by XXREAL_1: 235;

 end;

 theorem :: RCOMP_3:27



 Th27: for X be non empty interval Subset of REAL st X is bounded_below & not X is bounded_above & not ( lower_bound X) in X holds X = ( right_open_halfline ( lower_bound X))

 proof

 let X be non empty interval Subset of REAL such that

 A1: X is bounded_below and

 A2: not X is bounded_above and

 A3: not ( lower_bound X) in X;

 thus X c= ( right_open_halfline ( lower_bound X)) by A1, A3, Th26;

 let x be object;

 assume

 A4: x in ( right_open_halfline ( lower_bound X));

 then

 reconsider x as Real;

 not x is UpperBound of X by A2;

 then

 consider r be ExtReal such that

 A5: r in X & x < r by XXREAL_2:def 1;

 ( lower_bound X) < x by A4, XXREAL_1: 235;

 then (( lower_bound X) - ( lower_bound X)) < (x - ( lower_bound X)) by XREAL_1: 14;

 then

 consider s such that

 A6: s in X & s < (( lower_bound X) + (x - ( lower_bound X))) by A1, SEQ_4:def 2;

 reconsider r as Real by A5;

 [.s, r.] c= X & x in [.s, r.] by A5, A6, XXREAL_1: 1, XXREAL_2:def 12;

 hence thesis;

 end;

 theorem :: RCOMP_3:28



 Th28: for X be interval Subset of REAL st not X is bounded_above & not X is bounded_below holds X = REAL

 proof

 let X be interval Subset of REAL ;

 assume that

 A1: not X is bounded_above and

 A2: not X is bounded_below;

 thus X c= REAL ;

 let x be object;

 assume x in REAL ;

 then

 reconsider x as Real;

 not x is UpperBound of X by A1;

 then

 consider r be ExtReal such that

 A3: r in X & r > x by XXREAL_2:def 1;

 reconsider r as Real by A3;

 not x is LowerBound of X by A2;

 then

 consider s be ExtReal such that

 A4: s in X & s < x by XXREAL_2:def 2;

 reconsider s as Real by A4;

 [.s, r.] c= X & x in [.s, r.] by A3, A4, XXREAL_1: 1, XXREAL_2:def 12;

 hence thesis;

 end;

 theorem :: RCOMP_3:29



 Th29: for X be interval Subset of REAL holds X is empty or X = REAL or (ex a st X = ( left_closed_halfline a)) or (ex a st X = ( left_open_halfline a)) or (ex a st X = ( right_closed_halfline a)) or (ex a st X = ( right_open_halfline a)) or (ex a, b st a <= b & X = [.a, b.]) or (ex a, b st a < b & X = [.a, b.[) or (ex a, b st a < b & X = ].a, b.]) or ex a, b st a < b & X = ].a, b.[

 proof

 let X be interval Subset of REAL ;

 assume X is non empty;

 then

 reconsider X as non empty interval Subset of REAL ;

 per cases ;

 suppose X is real-bounded;

 then

 reconsider X as non empty real-bounded interval Subset of REAL ;

 per cases ;

 suppose X is trivial;

 then

 consider x be object such that

 A1: X = {x} by ZFMISC_1: 131;

 x in X by A1, TARSKI:def 1;

 then

 reconsider x as Real;

 X = [.x, x.] by A1, XXREAL_1: 17;

 hence thesis;

 end;

 suppose X is non trivial;

 then ex p,q be object st p in X & q in X & p <> q;

 then

 A2: ( lower_bound X) < ( upper_bound X) by SEQ_4: 12;

 per cases ;

 suppose ( upper_bound X) in X & ( lower_bound X) in X;

 then X = [.( lower_bound X), ( upper_bound X).] by Th13;

 hence thesis by A2;

 end;

 suppose ( upper_bound X) in X & not ( lower_bound X) in X;

 then X = ].( lower_bound X), ( upper_bound X).] by Th15;

 hence thesis by A2;

 end;

 suppose not ( upper_bound X) in X & ( lower_bound X) in X;

 then X = [.( lower_bound X), ( upper_bound X).[ by Th17;

 hence thesis by A2;

 end;

 suppose not ( upper_bound X) in X & not ( lower_bound X) in X;

 then X = ].( lower_bound X), ( upper_bound X).[ by Th19;

 hence thesis by A2;

 end;

 end;

 end;

 suppose

 A3: not X is real-bounded;

 per cases by A3;

 suppose

 A4: not X is bounded_below & X is bounded_above;

 per cases ;

 suppose ( upper_bound X) in X;

 then X = ( left_closed_halfline ( upper_bound X)) by A4, Th21;

 hence thesis;

 end;

 suppose not ( upper_bound X) in X;

 then X = ( left_open_halfline ( upper_bound X)) by A4, Th23;

 hence thesis;

 end;

 end;

 suppose

 A5: not X is bounded_above & X is bounded_below;

 per cases ;

 suppose ( lower_bound X) in X;

 then X = ( right_closed_halfline ( lower_bound X)) by A5, Th25;

 hence thesis;

 end;

 suppose not ( lower_bound X) in X;

 then X = ( right_open_halfline ( lower_bound X)) by A5, Th27;

 hence thesis;

 end;

 end;

 suppose not X is bounded_above & not X is bounded_below;

 hence thesis by Th28;

 end;

 end;

 end;

 theorem :: RCOMP_3:30



 Th30: for X be non empty interval Subset of REAL st not r in X holds r <= ( lower_bound X) or ( upper_bound X) <= r

 proof

 let X be non empty interval Subset of REAL such that

 A1: not r in X;

 per cases by Th29;

 suppose X = REAL ;

 hence thesis by A1, XREAL_0:def 1;

 end;

 suppose ex a st X = ( left_closed_halfline a);

 then

 consider a such that

 A2: X = ( left_closed_halfline a);

 ( upper_bound X) = a by A2, Th9;

 hence thesis by A1, A2, XXREAL_1: 234;

 end;

 suppose ex a st X = ( left_open_halfline a);

 then

 consider a such that

 A3: X = ( left_open_halfline a);

 ( upper_bound X) = a by A3, Th10;

 hence thesis by A1, A3, XXREAL_1: 233;

 end;

 suppose ex a st X = ( right_closed_halfline a);

 then

 consider a such that

 A4: X = ( right_closed_halfline a);

 ( lower_bound X) = a by A4, Th11;

 hence thesis by A1, A4, XXREAL_1: 236;

 end;

 suppose ex a st X = ( right_open_halfline a);

 then

 consider a such that

 A5: X = ( right_open_halfline a);

 ( lower_bound X) = a by A5, Th12;

 hence thesis by A1, A5, XXREAL_1: 235;

 end;

 suppose ex a, b st a <= b & X = [.a, b.];

 then

 consider a, b such that

 A6: a <= b and

 A7: X = [.a, b.];

 ( lower_bound X) = a & ( upper_bound X) = b by A6, A7, JORDAN5A: 19;

 hence thesis by A1, A7, XXREAL_1: 1;

 end;

 suppose ex a, b st a < b & X = [.a, b.[;

 then

 consider a, b such that

 A8: a < b and

 A9: X = [.a, b.[;

 ( lower_bound X) = a & ( upper_bound X) = b by A8, A9, Th4, Th5;

 hence thesis by A1, A9, XXREAL_1: 3;

 end;

 suppose ex a, b st a < b & X = ].a, b.];

 then

 consider a, b such that

 A10: a < b and

 A11: X = ].a, b.];

 ( lower_bound X) = a & ( upper_bound X) = b by A10, A11, Th6, Th7;

 hence thesis by A1, A11, XXREAL_1: 2;

 end;

 suppose ex a, b st a < b & X = ].a, b.[;

 then

 consider a, b such that

 A12: a < b and

 A13: X = ].a, b.[;

 ( lower_bound X) = a & ( upper_bound X) = b by A12, A13, TOPREAL6: 17;

 hence thesis by A1, A13, XXREAL_1: 4;

 end;

 end;

 theorem :: RCOMP_3:31



 Th31: for X,Y be non empty real-bounded interval Subset of REAL st ( lower_bound X) <= ( lower_bound Y) & ( upper_bound Y) <= ( upper_bound X) & (( lower_bound X) = ( lower_bound Y) & ( lower_bound Y) in Y implies ( lower_bound X) in X) & (( upper_bound X) = ( upper_bound Y) & ( upper_bound Y) in Y implies ( upper_bound X) in X) holds Y c= X

 proof

 let X,Y be non empty real-bounded interval Subset of REAL such that

 A1: ( lower_bound X) <= ( lower_bound Y) and

 A2: ( upper_bound Y) <= ( upper_bound X) and

 A3: ( lower_bound X) = ( lower_bound Y) & ( lower_bound Y) in Y implies ( lower_bound X) in X and

 A4: ( upper_bound X) = ( upper_bound Y) & ( upper_bound Y) in Y implies ( upper_bound X) in X;

 let x be object;

 assume

 A5: x in Y;

 then

 reconsider x as Real;



 A6: Y c= [.( lower_bound Y), ( upper_bound Y).] by XXREAL_2: 69;

 then

 A7: ( lower_bound Y) <= x by A5, XXREAL_1: 1;

 then

 A8: ( lower_bound X) <= x by A1, XXREAL_0: 2;



 A9: x <= ( upper_bound Y) by A5, A6, XXREAL_1: 1;

 then

 A10: x <= ( upper_bound X) by A2, XXREAL_0: 2;

 per cases by Th29;

 suppose X = ( [#] REAL );

 hence thesis;

 end;

 suppose (ex a st X = ( left_closed_halfline a)) or (ex a st X = ( left_open_halfline a)) or (ex a st X = ( right_closed_halfline a)) or ex a st X = ( right_open_halfline a);

 hence thesis;

 end;

 suppose ex a, b st a <= b & X = [.a, b.];

 then

 consider a, b such that

 A11: a <= b and

 A12: X = [.a, b.];

 ( lower_bound X) = a & ( upper_bound X) = b by A11, A12, JORDAN5A: 19;

 hence thesis by A8, A10, A12, XXREAL_1: 1;

 end;

 suppose ex a, b st a < b & X = [.a, b.[;

 then

 consider a, b such that

 A13: a < b and

 A14: X = [.a, b.[;



 A15: ( lower_bound X) = a by A13, A14, Th4;



 A16: ( upper_bound X) = b by A13, A14, Th5;

 per cases by Th29;

 suppose Y = ( [#] REAL );

 hence thesis;

 end;

 suppose (ex a st Y = ( left_closed_halfline a)) or (ex a st Y = ( left_open_halfline a)) or (ex a st Y = ( right_closed_halfline a)) or ex a st Y = ( right_open_halfline a);

 hence thesis;

 end;

 suppose ex a, b st a <= b & Y = [.a, b.];

 then

 consider a1,b1 be Real such that

 A17: a1 <= b1 & Y = [.a1, b1.];



 A18: ( upper_bound Y) = b1 by A17, JORDAN5A: 19;

 then b1 < b by A2, A4, A14, A16, A17, XXREAL_0: 1, XXREAL_1: 1, XXREAL_1: 3;

 then x < b by A9, A18, XXREAL_0: 2;

 hence thesis by A8, A14, A15, XXREAL_1: 3;

 end;

 suppose ex a, b st a < b & Y = [.a, b.[;

 then

 consider a1,b1 be Real such that

 A19: a1 < b1 & Y = [.a1, b1.[;

 ( upper_bound Y) = b1 & x < b1 by A5, A19, Th5, XXREAL_1: 3;

 then x < b by A2, A16, XXREAL_0: 2;

 hence thesis by A8, A14, A15, XXREAL_1: 3;

 end;

 suppose ex a, b st a < b & Y = ].a, b.];

 then

 consider a1,b1 be Real such that

 A20: a1 < b1 & Y = ].a1, b1.];



 A21: ( upper_bound Y) = b1 by A20, Th7;

 then b1 < b by A2, A4, A14, A16, A20, XXREAL_0: 1, XXREAL_1: 2, XXREAL_1: 3;

 then x < b by A9, A21, XXREAL_0: 2;

 hence thesis by A8, A14, A15, XXREAL_1: 3;

 end;

 suppose ex a, b st a < b & Y = ].a, b.[;

 then

 consider a1,b1 be Real such that

 A22: a1 < b1 & Y = ].a1, b1.[;

 ( upper_bound Y) = b1 & x < b1 by A5, A22, TOPREAL6: 17, XXREAL_1: 4;

 then x < b by A2, A16, XXREAL_0: 2;

 hence thesis by A8, A14, A15, XXREAL_1: 3;

 end;

 end;

 suppose ex a, b st a < b & X = ].a, b.];

 then

 consider a, b such that

 A23: a < b and

 A24: X = ].a, b.];



 A25: ( lower_bound X) = a by A23, A24, Th6;



 A26: ( upper_bound X) = b by A23, A24, Th7;

 per cases by Th29;

 suppose Y = ( [#] REAL );

 hence thesis;

 end;

 suppose (ex a st Y = ( left_closed_halfline a)) or (ex a st Y = ( left_open_halfline a)) or (ex a st Y = ( right_closed_halfline a)) or ex a st Y = ( right_open_halfline a);

 hence thesis;

 end;

 suppose ex a, b st a <= b & Y = [.a, b.];

 then

 consider a1,b1 be Real such that

 A27: a1 <= b1 & Y = [.a1, b1.];



 A28: ( lower_bound Y) = a1 by A27, JORDAN5A: 19;

 then a < a1 by A1, A3, A24, A25, A27, XXREAL_0: 1, XXREAL_1: 1, XXREAL_1: 2;

 then a < x by A7, A28, XXREAL_0: 2;

 hence thesis by A10, A24, A26, XXREAL_1: 2;

 end;

 suppose ex a, b st a < b & Y = [.a, b.[;

 then

 consider a1,b1 be Real such that

 A29: a1 < b1 and

 A30: Y = [.a1, b1.[;

 ( lower_bound Y) = a1 by A29, A30, Th4;

 then

 A31: a < a1 by A1, A3, A24, A25, A29, A30, XXREAL_0: 1, XXREAL_1: 2, XXREAL_1: 3;

 a1 <= x by A5, A30, XXREAL_1: 3;

 then a < x by A31, XXREAL_0: 2;

 hence thesis by A10, A24, A26, XXREAL_1: 2;

 end;

 suppose ex a, b st a < b & Y = ].a, b.];

 then

 consider a1,b1 be Real such that

 A32: a1 < b1 & Y = ].a1, b1.];

 ( lower_bound Y) = a1 & a1 < x by A5, A32, Th6, XXREAL_1: 2;

 then a < x by A1, A25, XXREAL_0: 2;

 hence thesis by A10, A24, A26, XXREAL_1: 2;

 end;

 suppose ex a, b st a < b & Y = ].a, b.[;

 then

 consider a1,b1 be Real such that

 A33: a1 < b1 & Y = ].a1, b1.[;

 ( lower_bound Y) = a1 & a1 < x by A5, A33, TOPREAL6: 17, XXREAL_1: 4;

 then a < x by A1, A25, XXREAL_0: 2;

 hence thesis by A10, A24, A26, XXREAL_1: 2;

 end;

 end;

 suppose ex a, b st a < b & X = ].a, b.[;

 then

 consider a, b such that

 A34: a < b and

 A35: X = ].a, b.[;



 A36: ( lower_bound X) = a by A34, A35, TOPREAL6: 17;



 A37: ( upper_bound X) = b by A34, A35, TOPREAL6: 17;

 per cases by Th29;

 suppose Y = ( [#] REAL );

 hence thesis;

 end;

 suppose (ex a st Y = ( left_closed_halfline a)) or (ex a st Y = ( left_open_halfline a)) or (ex a st Y = ( right_closed_halfline a)) or ex a st Y = ( right_open_halfline a);

 hence thesis;

 end;

 suppose ex a, b st a <= b & Y = [.a, b.];

 then

 consider a1,b1 be Real such that

 A38: a1 <= b1 and

 A39: Y = [.a1, b1.];

 ( upper_bound Y) = b1 by A38, A39, JORDAN5A: 19;

 then

 A40: b1 < b by A2, A4, A35, A37, A38, A39, XXREAL_0: 1, XXREAL_1: 1, XXREAL_1: 4;

 x <= b1 by A5, A39, XXREAL_1: 1;

 then

 A41: x < b by A40, XXREAL_0: 2;



 A42: ( lower_bound Y) = a1 by A38, A39, JORDAN5A: 19;

 then a < a1 by A1, A3, A35, A36, A38, A39, XXREAL_0: 1, XXREAL_1: 1, XXREAL_1: 4;

 then a < x by A7, A42, XXREAL_0: 2;

 hence thesis by A35, A41, XXREAL_1: 4;

 end;

 suppose ex a, b st a < b & Y = [.a, b.[;

 then

 consider a1,b1 be Real such that

 A43: a1 < b1 and

 A44: Y = [.a1, b1.[;

 ( lower_bound Y) = a1 by A43, A44, Th4;

 then

 A45: a < a1 by A1, A3, A35, A36, A43, A44, XXREAL_0: 1, XXREAL_1: 3, XXREAL_1: 4;

 a1 <= x by A5, A44, XXREAL_1: 3;

 then

 A46: a < x by A45, XXREAL_0: 2;

 ( upper_bound Y) = b1 & x < b1 by A5, A43, A44, Th5, XXREAL_1: 3;

 then x < b by A2, A37, XXREAL_0: 2;

 hence thesis by A35, A46, XXREAL_1: 4;

 end;

 suppose ex a, b st a < b & Y = ].a, b.];

 then

 consider a1,b1 be Real such that

 A47: a1 < b1 and

 A48: Y = ].a1, b1.];

 ( upper_bound Y) = b1 by A47, A48, Th7;

 then

 A49: b1 < b by A2, A4, A35, A37, A47, A48, XXREAL_0: 1, XXREAL_1: 2, XXREAL_1: 4;

 x <= b1 by A5, A48, XXREAL_1: 2;

 then

 A50: x < b by A49, XXREAL_0: 2;

 ( lower_bound Y) = a1 & a1 < x by A5, A47, A48, Th6, XXREAL_1: 2;

 then a < x by A1, A36, XXREAL_0: 2;

 hence thesis by A35, A50, XXREAL_1: 4;

 end;

 suppose ex a, b st a < b & Y = ].a, b.[;

 then

 consider a1,b1 be Real such that

 A51: a1 < b1 & Y = ].a1, b1.[;

 ( lower_bound Y) = a1 & a1 < x by A5, A51, TOPREAL6: 17, XXREAL_1: 4;

 then

 A52: a < x by A1, A36, XXREAL_0: 2;

 ( upper_bound Y) = b1 & x < b1 by A5, A51, TOPREAL6: 17, XXREAL_1: 4;

 then x < b by A2, A37, XXREAL_0: 2;

 hence thesis by A35, A52, XXREAL_1: 4;

 end;

 end;

 end;

 registration

 cluster open closed interval non empty non real-bounded for Subset of REAL ;

 existence

 proof

 take ( [#] REAL );

 thus thesis;

 end;

 end

 begin

 theorem :: RCOMP_3:32



 Th32: for X be Subset of R^1 st a <= b & X = [.a, b.] holds ( Fr X) = {a, b}

 proof

 let X be Subset of R^1 such that

 A1: a <= b and

 A2: X = [.a, b.];



 A3: ( Cl X) = ( Cl [.a, b.]) by A2, JORDAN5A: 24

 .= [.a, b.] by MEASURE6: 59;



 A4: ( [.a, b.] /\ (( left_closed_halfline a) \/ ( right_closed_halfline b))) = {a, b} by A1, Th8;

 set LO = ( R^1 ( left_open_halfline a)), RC = ( R^1 ( right_closed_halfline b)), RO = ( R^1 ( right_open_halfline b)), LC = ( R^1 ( left_closed_halfline a));



 A5: RC = ( right_closed_halfline b) by TOPREALB:def 3;



 A6: LC = ( left_closed_halfline a) by TOPREALB:def 3;



 A7: RO = ( right_open_halfline b) by TOPREALB:def 3;



 A8: LO = ( left_open_halfline a) by TOPREALB:def 3;

 then

 A9: ( [.a, b.] ` ) = (LO \/ RO) by A7, XXREAL_1: 385;

 ( Cl (X ` )) = ( Cl ( [.a, b.] ` )) by A2, JORDAN5A: 24, TOPMETR: 17

 .= (( Cl ( left_open_halfline a)) \/ ( Cl ( right_open_halfline b))) by A8, A7, A9, Th3

 .= (( Cl LO) \/ ( Cl ( right_open_halfline b))) by A8, JORDAN5A: 24

 .= (( Cl LO) \/ ( Cl RO)) by A7, JORDAN5A: 24

 .= (LC \/ ( Cl RO)) by A6, BORSUK_5: 51, TOPREALB:def 3

 .= (LC \/ RC) by A5, BORSUK_5: 49, TOPREALB:def 3

 .= (( left_closed_halfline a) \/ ( right_closed_halfline b)) by A5, TOPREALB:def 3;

 hence thesis by A3, A4, TOPS_1:def 2;

 end;

 theorem :: RCOMP_3:33

 for X be Subset of R^1 st a < b & X = ].a, b.[ holds ( Fr X) = {a, b}

 proof

 let X be Subset of R^1 such that

 A1: a < b and

 A2: X = ].a, b.[;



 A3: ( Cl X) = ( Cl ].a, b.[) by A2, JORDAN5A: 24

 .= [.a, b.] by A1, JORDAN5A: 26;

 set RC = ( R^1 ( right_closed_halfline b)), LC = ( R^1 ( left_closed_halfline a));



 A4: RC = ( right_closed_halfline b) & LC = ( left_closed_halfline a) by TOPREALB:def 3;

 then

 A5: ( ].a, b.[ ` ) = (LC \/ RC) by XXREAL_1: 398;



 A6: ( [.a, b.] /\ (( left_closed_halfline a) \/ ( right_closed_halfline b))) = {a, b} by A1, Th8;

 ( Cl (X ` )) = ( Cl ( ].a, b.[ ` )) by A2, JORDAN5A: 24, TOPMETR: 17

 .= (( Cl ( left_closed_halfline a)) \/ ( Cl ( right_closed_halfline b))) by A4, A5, Th3

 .= (( Cl ( left_closed_halfline a)) \/ ( right_closed_halfline b)) by MEASURE6: 59

 .= (( left_closed_halfline a) \/ ( right_closed_halfline b)) by MEASURE6: 59;

 hence thesis by A3, A6, TOPS_1:def 2;

 end;

 theorem :: RCOMP_3:34



 Th34: for X be Subset of R^1 st a < b & X = [.a, b.[ holds ( Fr X) = {a, b}

 proof

 let X be Subset of R^1 such that

 A1: a < b and

 A2: X = [.a, b.[;



 A3: ( Cl X) = [.a, b.] & ( [.a, b.] /\ (( left_closed_halfline a) \/ ( right_closed_halfline b))) = {a, b} by A1, A2, Th8, BORSUK_5: 35;

 set LO = ( R^1 ( left_open_halfline a)), RC = ( R^1 ( right_closed_halfline b)), LC = ( R^1 ( left_closed_halfline a));



 A4: RC = ( right_closed_halfline b) by TOPREALB:def 3;



 A5: LO = ( left_open_halfline a) by TOPREALB:def 3;

 then

 A6: ( [.a, b.[ ` ) = (LO \/ RC) by A4, XXREAL_1: 382;



 A7: LC = ( left_closed_halfline a) by TOPREALB:def 3;

 ( Cl (X ` )) = ( Cl ( [.a, b.[ ` )) by A2, JORDAN5A: 24, TOPMETR: 17

 .= (( Cl ( left_open_halfline a)) \/ ( Cl ( right_closed_halfline b))) by A5, A4, A6, Th3

 .= (( Cl LO) \/ ( Cl ( right_closed_halfline b))) by A5, JORDAN5A: 24

 .= (( Cl LO) \/ ( Cl RC)) by A4, JORDAN5A: 24

 .= (LC \/ ( Cl RC)) by A7, BORSUK_5: 51, TOPREALB:def 3

 .= (( left_closed_halfline a) \/ ( right_closed_halfline b)) by A4, A7, PRE_TOPC: 22;

 hence thesis by A3, TOPS_1:def 2;

 end;

 theorem :: RCOMP_3:35



 Th35: for X be Subset of R^1 st a < b & X = ].a, b.] holds ( Fr X) = {a, b}

 proof

 let X be Subset of R^1 such that

 A1: a < b and

 A2: X = ].a, b.];



 A3: ( Cl X) = [.a, b.] & ( [.a, b.] /\ (( left_closed_halfline a) \/ ( right_closed_halfline b))) = {a, b} by A1, A2, Th8, BORSUK_5: 36;



 A4: ( ].a, b.] ` ) = (( left_closed_halfline a) \/ ( right_open_halfline b)) by XXREAL_1: 399;

 set RO = ( R^1 ( right_open_halfline b)), LC = ( R^1 ( left_closed_halfline a));



 A5: RO = ( right_open_halfline b) by TOPREALB:def 3;



 A6: LC = ( left_closed_halfline a) by TOPREALB:def 3;

 ( Cl (X ` )) = ( Cl ( ].a, b.] ` )) by A2, JORDAN5A: 24, TOPMETR: 17

 .= (( Cl ( left_closed_halfline a)) \/ ( Cl ( right_open_halfline b))) by A4, Th3

 .= (( Cl LC) \/ ( Cl ( right_open_halfline b))) by A6, JORDAN5A: 24

 .= (( Cl LC) \/ ( Cl RO)) by A5, JORDAN5A: 24

 .= (LC \/ ( Cl RO)) by PRE_TOPC: 22

 .= (( left_closed_halfline a) \/ ( right_closed_halfline b)) by A6, BORSUK_5: 49, TOPREALB:def 3;

 hence thesis by A3, TOPS_1:def 2;

 end;

 theorem :: RCOMP_3:36

 for X be Subset of R^1 st X = [.a, b.] holds ( Int X) = ].a, b.[

 proof

 let X be Subset of R^1 such that

 A1: X = [.a, b.];



 A2: ( Int X) c= X by TOPS_1: 16;

 thus ( Int X) c= ].a, b.[

 proof

 let x be object;

 assume

 A3: x in ( Int X);

 then

 reconsider x as Point of R^1 ;

 A4:

 now

 now

 assume a > b;

 then X = ( {} R^1 ) by A1, XXREAL_1: 29;

 hence contradiction by A3;

 end;

 then ( Fr X) = {a, b} by A1, Th32;

 then

 A5: a in ( Fr X) & b in ( Fr X) by TARSKI:def 2;



 A6: ( Int X) misses ( Fr X) by TOPS_1: 39;

 assume x = a or x = b;

 hence contradiction by A3, A6, A5, XBOOLE_0: 3;

 end;

 x <= b by A1, A2, A3, XXREAL_1: 1;

 then

 A7: x < b by A4, XXREAL_0: 1;

 a <= x by A1, A2, A3, XXREAL_1: 1;

 then a < x by A4, XXREAL_0: 1;

 hence thesis by A7, XXREAL_1: 4;

 end;

 reconsider Y = ].a, b.[ as open Subset of R^1 by BORSUK_5: 39, TOPMETR: 17;

 Y c= ( Int X) by A1, TOPS_1: 24, XXREAL_1: 37;

 hence thesis;

 end;

 theorem :: RCOMP_3:37

 for X be Subset of R^1 st X = ].a, b.[ holds ( Int X) = ].a, b.[

 proof

 let X be Subset of R^1 ;

 assume

 A1: X = ].a, b.[;

 then

 reconsider X as open Subset of R^1 by BORSUK_5: 39;

 ( Int X) = X by TOPS_1: 23;

 hence thesis by A1;

 end;

 theorem :: RCOMP_3:38



 Th38: for X be Subset of R^1 st X = [.a, b.[ holds ( Int X) = ].a, b.[

 proof

 let X be Subset of R^1 such that

 A1: X = [.a, b.[;



 A2: ( Int X) c= X by TOPS_1: 16;

 thus ( Int X) c= ].a, b.[

 proof

 let x be object;

 assume

 A3: x in ( Int X);

 then

 reconsider x as Point of R^1 ;

 A4:

 now

 now

 assume a >= b;

 then X = ( {} R^1 ) by A1, XXREAL_1: 27;

 hence contradiction by A3;

 end;

 then ( Fr X) = {a, b} by A1, Th34;

 then

 A5: ( Int X) misses ( Fr X) & a in ( Fr X) by TARSKI:def 2, TOPS_1: 39;

 assume x = a;

 hence contradiction by A3, A5, XBOOLE_0: 3;

 end;

 a <= x by A1, A2, A3, XXREAL_1: 3;

 then

 A6: a < x by A4, XXREAL_0: 1;

 x < b by A1, A2, A3, XXREAL_1: 3;

 hence thesis by A6, XXREAL_1: 4;

 end;

 reconsider Y = ].a, b.[ as open Subset of R^1 by BORSUK_5: 39, TOPMETR: 17;

 Y c= ( Int X) by A1, TOPS_1: 24, XXREAL_1: 45;

 hence thesis;

 end;

 theorem :: RCOMP_3:39



 Th39: for X be Subset of R^1 st X = ].a, b.] holds ( Int X) = ].a, b.[

 proof

 let X be Subset of R^1 such that

 A1: X = ].a, b.];



 A2: ( Int X) c= X by TOPS_1: 16;

 thus ( Int X) c= ].a, b.[

 proof

 let x be object;

 assume

 A3: x in ( Int X);

 then

 reconsider x as Point of R^1 ;

 A4:

 now

 now

 assume a >= b;

 then X = ( {} R^1 ) by A1, XXREAL_1: 26;

 hence contradiction by A3;

 end;

 then ( Fr X) = {a, b} by A1, Th35;

 then

 A5: ( Int X) misses ( Fr X) & b in ( Fr X) by TARSKI:def 2, TOPS_1: 39;

 assume x = b;

 hence contradiction by A3, A5, XBOOLE_0: 3;

 end;

 x <= b by A1, A2, A3, XXREAL_1: 2;

 then

 A6: x < b by A4, XXREAL_0: 1;

 a < x by A1, A2, A3, XXREAL_1: 2;

 hence thesis by A6, XXREAL_1: 4;

 end;

 reconsider Y = ].a, b.[ as open Subset of R^1 by BORSUK_5: 39, TOPMETR: 17;

 Y c= ( Int X) by A1, TOPS_1: 24, XXREAL_1: 41;

 hence thesis;

 end;

 registration

 let T be real-membered TopStruct, X be interval Subset of T;

 cluster (T | X) -> interval;

 coherence by PRE_TOPC:def 5;

 end

 registration

 let A be interval Subset of REAL ;

 cluster ( R^1 A) -> interval;

 coherence by TOPREALB:def 3;

 end

 registration

 cluster connected -> interval for Subset of R^1 ;

 coherence by BORSUK_5: 77;

 cluster interval -> connected for Subset of R^1 ;

 coherence

 proof

 let X be Subset of R^1 such that

 A1: X is interval;



 A2: X is Subset of REAL by MEMBERED: 3;

 per cases by A1, A2, Th29;

 suppose X is empty;

 then

 reconsider A = X as empty Subset of R^1 ;

 A is interval;

 hence thesis;

 end;

 suppose X = REAL ;

 then

 reconsider A = X as non empty interval Subset of R^1 ;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 suppose ex a st X = ( left_closed_halfline a);

 then

 consider a such that

 A3: X = ( left_closed_halfline a);

 reconsider A = X as non empty interval Subset of R^1 by A3;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 suppose ex a st X = ( left_open_halfline a);

 then

 consider a such that

 A4: X = ( left_open_halfline a);

 reconsider A = X as non empty interval Subset of R^1 by A4;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 suppose ex a st X = ( right_closed_halfline a);

 then

 consider a such that

 A5: X = ( right_closed_halfline a);

 reconsider A = X as non empty interval Subset of R^1 by A5;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 suppose ex a st X = ( right_open_halfline a);

 then

 consider a such that

 A6: X = ( right_open_halfline a);

 reconsider A = X as non empty interval Subset of R^1 by A6;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 suppose ex a, b st a <= b & X = [.a, b.];

 then

 reconsider A = X as non empty interval Subset of R^1 by XXREAL_1: 1;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 suppose ex a, b st a < b & X = [.a, b.[;

 then

 reconsider A = X as non empty interval Subset of R^1 by XXREAL_1: 3;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 suppose ex a, b st a < b & X = ].a, b.];

 then

 reconsider A = X as non empty interval Subset of R^1 by XXREAL_1: 2;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 suppose ex a, b st a < b & X = ].a, b.[;

 then

 reconsider A = X as non empty interval Subset of R^1 by XXREAL_1: 33;

 ( R^1 | A) is connected;

 hence ( R^1 | X) is connected;

 end;

 end;

 end

 begin

 registration

 let r;

 cluster ( Closed-Interval-TSpace (r,r)) -> 1 -element;

 coherence

 proof

 {r} is 1 -element & the carrier of ( Closed-Interval-TSpace (r,r)) = [.r, r.] by TOPMETR: 18;

 hence the carrier of ( Closed-Interval-TSpace (r,r)) is 1 -element by XXREAL_1: 17;

 end;

 end

 theorem :: RCOMP_3:40

 r <= s implies for A be Subset of ( Closed-Interval-TSpace (r,s)) holds A is real-bounded Subset of REAL

 proof

 assume r <= s;

 then

 A1: the carrier of ( Closed-Interval-TSpace (r,s)) = [.r, s.] by TOPMETR: 18;

 let A be Subset of ( Closed-Interval-TSpace (r,s));

 A is bounded_above bounded_below by A1, XXREAL_2: 43, XXREAL_2: 44;

 hence thesis by A1, XBOOLE_1: 1;

 end;

 theorem :: RCOMP_3:41



 Th41: r <= s implies for X be Subset of ( Closed-Interval-TSpace (r,s)) st X = [.a, b.[ & r < a & b <= s holds ( Int X) = ].a, b.[

 proof

 set L = ( Closed-Interval-TSpace (r,s));

 set c = ((r + a) / 2);

 set C1 = ( R^1 ].c, b.[);



 A1: C1 = ].c, b.[ by TOPREALB:def 3;

 assume r <= s;

 then

 A2: the carrier of L = [.r, s.] by TOPMETR: 18;

 let X be Subset of ( Closed-Interval-TSpace (r,s)) such that

 A3: X = [.a, b.[ and

 A4: r < a and

 A5: b <= s;



 A6: r < c by A4, XREAL_1: 226;



 A7: C1 c= the carrier of L

 proof

 let x be object;

 assume

 A8: x in C1;

 then

 reconsider x as Real;

 x < b by A1, A8, XXREAL_1: 4;

 then

 A9: x <= s by A5, XXREAL_0: 2;

 c < x by A1, A8, XXREAL_1: 4;

 then r <= x by A6, XXREAL_0: 2;

 hence thesis by A2, A9, XXREAL_1: 1;

 end;

 reconsider A = X as Subset of R^1 by PRE_TOPC: 11;



 A10: c < a by A4, XREAL_1: 226;

 A c= C1

 proof

 let x be object;

 assume

 A11: x in A;

 then

 reconsider x as Real;

 a <= x by A3, A11, XXREAL_1: 3;

 then

 A12: c < x by A10, XXREAL_0: 2;

 x < b by A3, A11, XXREAL_1: 3;

 hence thesis by A1, A12, XXREAL_1: 4;

 end;

 then ( Int A) = ( Int X) by A7, TOPS_3: 57;

 hence thesis by A3, Th38;

 end;

 theorem :: RCOMP_3:42



 Th42: r <= s implies for X be Subset of ( Closed-Interval-TSpace (r,s)) st X = ].a, b.] & r <= a & b < s holds ( Int X) = ].a, b.[

 proof

 set L = ( Closed-Interval-TSpace (r,s));

 set c = ((b + s) / 2);

 set C1 = ( R^1 ].a, c.[);



 A1: C1 = ].a, c.[ by TOPREALB:def 3;

 assume r <= s;

 then

 A2: the carrier of L = [.r, s.] by TOPMETR: 18;

 let X be Subset of ( Closed-Interval-TSpace (r,s)) such that

 A3: X = ].a, b.] and

 A4: r <= a and

 A5: b < s;



 A6: c < s by A5, XREAL_1: 226;



 A7: C1 c= the carrier of L

 proof

 let x be object;

 assume

 A8: x in C1;

 then

 reconsider x as Real;

 x < c by A1, A8, XXREAL_1: 4;

 then

 A9: x <= s by A6, XXREAL_0: 2;

 a < x by A1, A8, XXREAL_1: 4;

 then r <= x by A4, XXREAL_0: 2;

 hence thesis by A2, A9, XXREAL_1: 1;

 end;

 reconsider A = X as Subset of R^1 by PRE_TOPC: 11;



 A10: b < c by A5, XREAL_1: 226;

 A c= C1

 proof

 let x be object;

 assume

 A11: x in A;

 then

 reconsider x as Real;

 x <= b by A3, A11, XXREAL_1: 2;

 then

 A12: x < c by A10, XXREAL_0: 2;

 a < x by A3, A11, XXREAL_1: 2;

 hence thesis by A1, A12, XXREAL_1: 4;

 end;

 then ( Int A) = ( Int X) by A7, TOPS_3: 57;

 hence thesis by A3, Th39;

 end;

 theorem :: RCOMP_3:43



 Th43: for X be Subset of ( Closed-Interval-TSpace (r,s)), Y be Subset of REAL st X = Y holds X is connected iff Y is interval

 proof

 let X be Subset of ( Closed-Interval-TSpace (r,s)), Y be Subset of REAL such that

 A1: X = Y;

 reconsider Z = X as Subset of R^1 by A1, TOPMETR: 17;

 hereby

 assume X is connected;

 then Z is connected by CONNSP_1: 23;

 hence Y is interval by A1;

 end;

 assume Y is interval;

 then Z is connected by A1;

 hence thesis by CONNSP_1: 23;

 end;

 registration

 let T be TopSpace;

 cluster open closed connected for Subset of T;

 existence

 proof

 take ( {} T);

 thus thesis;

 end;

 end

 registration

 let T be non empty connected TopSpace;

 cluster non empty open closed connected for Subset of T;

 existence

 proof

 take ( [#] T);

 thus thesis by CONNSP_1: 27;

 end;

 end

 theorem :: RCOMP_3:44



 Th44: r <= s implies for X be open connected Subset of ( Closed-Interval-TSpace (r,s)) holds X is empty or X = [.r, s.] or (ex a be Real st r < a & a <= s & X = [.r, a.[) or (ex a be Real st r <= a & a < s & X = ].a, s.]) or ex a,b be Real st r <= a & a < b & b <= s & X = ].a, b.[

 proof

 set L = ( Closed-Interval-TSpace (r,s));

 assume

 A1: r <= s;

 then

 A2: the carrier of L = [.r, s.] by TOPMETR: 18;

 let X be open connected Subset of L;

 X is bounded_above bounded_below Subset of REAL by A2, XBOOLE_1: 1, XXREAL_2: 43, XXREAL_2: 44;

 then

 reconsider Y = X as real-bounded interval Subset of REAL by Th43;



 A3: the carrier of L = ( [#] L) & L is connected by A1, TREAL_1: 20;



 A4: s in [.r, s.] by A1, XXREAL_1: 1;



 A5: r in [.r, s.] by A1, XXREAL_1: 1;

 per cases by Th29;

 suppose Y is empty or Y = ( [#] REAL );

 hence thesis;

 end;

 suppose (ex a st Y = ( left_closed_halfline a)) or (ex a st Y = ( left_open_halfline a)) or (ex a st Y = ( right_closed_halfline a)) or ex a st Y = ( right_open_halfline a);

 hence thesis;

 end;

 suppose ex a, b st a <= b & Y = [.a, b.];

 then

 consider a, b such that

 A6: a <= b and

 A7: Y = [.a, b.];



 A8: X <> ( {} L) by A6, A7, XXREAL_1: 1;



 A9: r <= a & b <= s by A2, A6, A7, XXREAL_1: 50;

 then

 A10: X is closed by A7, TOPREALA: 23;

 now

 assume

 A11: r <> a or b <> s;

 per cases by A9, A11, XXREAL_0: 1;

 suppose r < a;

 then not r in X by A7, XXREAL_1: 1;

 hence contradiction by A2, A3, A5, A8, A10, CONNSP_1: 13;

 end;

 suppose b < s;

 then not s in X by A7, XXREAL_1: 1;

 hence contradiction by A2, A3, A4, A8, A10, CONNSP_1: 13;

 end;

 end;

 hence thesis by A7;

 end;

 suppose ex a, b st a < b & Y = [.a, b.[;

 then

 consider a, b such that

 A12: a a;

 then

 A16: r < a by A15, XXREAL_0: 1;

 now

 ( Int X) = ].a, b.[ by A1, A13, A14, A16, Th41;

 then

 A17: not a in ( Int X) by XXREAL_1: 4;

 assume ( Int X) = X;

 hence contradiction by A12, A13, A17, XXREAL_1: 3;

 end;

 hence contradiction by TOPS_1: 23;

 end;

 hence thesis by A12, A13, A14;

 end;

 suppose ex a, b st a < b & Y = ].a, b.];

 then

 consider a, b such that

 A18: a s;

 then

 A22: b < s by A21, XXREAL_0: 1;

 now

 ( Int X) = ].a, b.[ by A1, A19, A20, A22, Th42;

 then

 A23: not b in ( Int X) by XXREAL_1: 4;

 assume ( Int X) = X;

 hence contradiction by A18, A19, A23, XXREAL_1: 2;

 end;

 hence contradiction by TOPS_1: 23;

 end;

 hence thesis by A18, A19, A20;

 end;

 suppose ex a, b st a < b & Y = ].a, b.[;

 then

 consider a, b such that

 A24: a < b & Y = ].a, b.[;

 r <= a & b <= s by A2, A24, XXREAL_1: 51;

 hence thesis by A24;

 end;

 end;

 begin

 deffunc F( set) = $1;

 defpred P[ set, set] means $1 c= $2;

 theorem :: RCOMP_3:45



 Th45: for T be 1-sorted, F be finite Subset-Family of T holds for F1 be Subset-Family of T st F is Cover of T & F1 = (F \ { X where X be Subset of T : X in F & ex Y be Subset of T st Y in F & X c< Y }) holds F1 is Cover of T

 proof

 let T be 1-sorted, F be finite Subset-Family of T, F1 be Subset-Family of T such that

 A1: the carrier of T c= ( union F) and

 A2: F1 = (F \ { X where X be Subset of T : X in F & ex Y be Subset of T st Y in F & X c< Y });

 set ZAW = { X where X be Subset of T : X in F & ex Y be Subset of T st Y in F & X c< Y };

 thus the carrier of T c= ( union F1)

 proof

 let t be object;

 assume t in the carrier of T;

 then

 consider Z be set such that

 A3: t in Z and

 A4: Z in F by A1, TARSKI:def 4;

 set ALL = { X where X be Subset of T : Z c< X & X in F };

 per cases ;

 suppose

 A5: ALL is empty;

 now

 assume Z in ZAW;

 then

 consider X be Subset of T such that

 A6: Z = X and X in F and

 A7: ex Y be Subset of T st Y in F & X c< Y;

 consider Y be Subset of T such that

 A8: Y in F & X c< Y by A7;

 Y in ALL by A6, A8;

 hence contradiction by A5;

 end;

 then Z in F1 by A2, A4, XBOOLE_0:def 5;

 hence thesis by A3, TARSKI:def 4;

 end;

 suppose ALL is non empty;

 then

 consider w be object such that

 A9: w in ALL;

 consider R be Relation of ALL such that

 A10: for x,y be set holds [x, y] in R iff x in ALL & y in ALL & P[x, y] from RELSET_1:sch 5;



 A11: R is_reflexive_in ALL by A10;

 then

 A12: ( field R) = ALL by ORDERS_1: 13;



 A13: R partially_orders ALL

 proof

 thus R is_reflexive_in ALL by A11;

 thus R is_transitive_in ALL

 proof

 let x,y,z be object;

 assume that

 A14: x in ALL and y in ALL and

 A15: z in ALL;

 assume

 A16: [x, y] in R & [y, z] in R;

 reconsider x, y, z as set by TARSKI: 1;

 x c= y & y c= z by A10, A16;

 then x c= z;

 hence thesis by A10, A14, A15;

 end;

 let x,y be object;

 assume that x in ALL and y in ALL;

 assume

 A17: [x, y] in R & [y, x] in R;

 reconsider x, y as set by TARSKI: 1;

 x c= y & y c= x by A10, A17;

 hence thesis by XBOOLE_0:def 10;

 end;



 A18: R is reflexive by A11, A12;

 ALL has_upper_Zorn_property_wrt R

 proof

 let Y be set such that

 A19: Y c= ALL and

 A20: (R |_2 Y) is being_linear-order;

 per cases ;

 suppose

 A21: Y is non empty;

 defpred U[ set] means $1 is non empty & $1 c= Y implies ( union $1) in Y;

 take ( union Y);



 A22: U[ {} ];



 A23: for A,B be set st A in Y & B in Y holds (A \/ B) in Y

 proof



 A24: (R |_2 Y) c= R by XBOOLE_1: 17;

 (R |_2 Y) is connected by A20;

 then

 A25: (R |_2 Y) is_connected_in ( field (R |_2 Y));

 let A,B be set such that

 A26: A in Y & B in Y;

 ( field (R |_2 Y)) = Y by A12, A18, A19, ORDERS_1: 71;

 then [A, B] in (R |_2 Y) or [B, A] in (R |_2 Y) or A = B by A26, A25;

 then A c= B or B c= A by A10, A24;

 hence thesis by A26, XBOOLE_1: 12;

 end;



 A27: for x,B be set st x in Y & B c= Y & U[B] holds U[(B \/ {x})]

 proof

 let x,B be set such that

 A28: x in Y and

 A29: B c= Y & U[B] and (B \/ {x}) is non empty and (B \/ {x}) c= Y;



 A30: ( union {x}) = x by ZFMISC_1: 25;

 per cases ;

 suppose B is empty;

 hence thesis by A28, ZFMISC_1: 25;

 end;

 suppose B is non empty;

 then (x \/ ( union B)) in Y by A23, A28, A29;

 hence thesis by A30, ZFMISC_1: 78;

 end;

 end;

 consider y be object such that

 A31: y in Y by A21;

 y in ALL by A19, A31;

 then

 consider X be Subset of T such that

 A32: X = y and

 A33: Z c< X and X in F;



 A34: X c= ( union Y) by A31, A32, ZFMISC_1: 74;

 then

 A35: Z <> ( union Y) by A33, XBOOLE_0:def 8;

 Z c= X by A33;

 then Z c= ( union Y) by A34;

 then

 A36: Z c< ( union Y) by A35;



 A37: ALL c= F

 proof

 let x be object;

 assume x in ALL;

 then ex X be Subset of T st X = x & Z c< X & X in F;

 hence thesis;

 end;

 then

 A38: Y c= F by A19;



 A39: Y is finite by A19, A37;

 U[Y] from FINSET_1:sch 2( A39, A22, A27);

 then ( union Y) in F by A21, A38;

 hence

 A40: ( union Y) in ALL by A36;

 let z be set;

 assume

 A41: z in Y;

 then P[z, ( union Y)] by ZFMISC_1: 74;

 hence thesis by A10, A19, A40, A41;

 end;

 suppose

 A42: Y is empty;

 reconsider w as set by TARSKI: 1;

 take w;

 thus w in ALL by A9;

 thus thesis by A42;

 end;

 end;

 then

 consider M be set such that

 A43: M is_maximal_in R by A12, A13, ORDERS_1: 63;



 A44: M in ( field R) by A43;

 then

 A45: ex X be Subset of T st X = M & Z c< X & X in F by A12;

 now

 assume M in ZAW;

 then

 consider H be Subset of T such that

 A46: M = H and H in F and

 A47: ex Y be Subset of T st Y in F & H c< Y;

 consider Y be Subset of T such that

 A48: Y in F and

 A49: H c< Y by A47;

 Z c< Y by A45, A46, A49, XBOOLE_1: 56;

 then

 A50: Y in ALL by A48;

 H c= Y by A49;

 then [M, Y] in R by A10, A12, A44, A46, A50;

 hence contradiction by A12, A43, A46, A49, A50;

 end;

 then

 A51: M in F1 by A2, A45, XBOOLE_0:def 5;

 Z c= M by A45;

 hence thesis by A3, A51, TARSKI:def 4;

 end;

 end;

 end;

 theorem :: RCOMP_3:46



 Th46: for S be 1 -element 1-sorted, s be Point of S, F be Subset-Family of S st F is Cover of S holds {s} in F

 proof

 let S be 1 -element 1-sorted, s be Point of S, F be Subset-Family of S such that

 A1: the carrier of S c= ( union F);

 consider d be Element of S such that

 A2: the carrier of S = {d} by TEX_1:def 1;

 s in the carrier of S;

 then

 consider Z be set such that

 A3: s in Z and

 A4: Z in F by A1, TARSKI:def 4;



 A5: s = d by ZFMISC_1:def 10;

 Z = {s}

 proof

 thus for x be object st x in Z holds x in {s} by A4, A2, A5;

 let x be object;

 thus thesis by A3, TARSKI:def 1;

 end;

 hence thesis by A4;

 end;

 definition

 let T be TopStruct, F be Subset-Family of T;

 :: RCOMP_3:def1

 attr F is connected means for X be Subset of T st X in F holds X is connected;

 end

 registration

 let T be TopSpace;

 cluster non empty open closed connected for Subset-Family of T;

 existence

 proof

 {( {} T)} c= ( bool the carrier of T)

 proof

 let x be object;

 assume x in {( {} T)};

 then x = ( {} T) by TARSKI:def 1;

 hence thesis;

 end;

 then

 reconsider F = {( {} T)} as Subset-Family of T;

 take F;

 thus F is non empty;

 thus for P be Subset of T holds P in F implies P is open by TARSKI:def 1;

 thus for P be Subset of T holds P in F implies P is closed by TARSKI:def 1;

 thus for P be Subset of T holds P in F implies P is connected by TARSKI:def 1;

 end;

 end

 reserve n,m for Nat,

F for Subset-Family of ( Closed-Interval-TSpace (r,s));



 Lm3: [.r, s.] in F & r <= s implies ( rng <* [.r, s.]*>) c= F & ( union ( rng <* [.r, s.]*>)) = [.r, s.] & for n be Nat st 1 <= n holds (n <= ( len <* [.r, s.]*>) implies ( <* [.r, s.]*> /. n) is non 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))))

 proof

 assume that

 A1: [.r, s.] in F and

 A2: r <= s;

 set f = <* [.r, s.]*>;



 A3: ( rng f) = { [.r, s.]} by FINSEQ_1: 38;

 thus ( rng f) c= F by A1, A3, TARSKI:def 1;

 thus ( union ( rng f)) = [.r, s.] by A3, ZFMISC_1: 25;

 let n be Nat;

 assume

 A4: 1 <= n;

 hereby

 assume n <= ( len f);

 then n <= 1 by FINSEQ_1: 39;

 then n = 1 by A4, XXREAL_0: 1;

 then (f /. n) = [.r, s.] by FINSEQ_4: 16;

 hence (f /. n) is non empty by A2, XXREAL_1: 1;

 end;

 hereby

 assume (n + 1) <= ( len f);

 then (n + 1) <= ( 0 + 1) by FINSEQ_1: 39;

 hence ( lower_bound (f /. n)) <= ( lower_bound (f /. (n + 1))) & ( upper_bound (f /. n)) <= ( upper_bound (f /. (n + 1))) & ( lower_bound (f /. (n + 1))) < ( upper_bound (f /. n)) by A4, XREAL_1: 6;

 end;

 assume (n + 2) <= ( len f);

 then ((n + 1) + 1) <= ( 0 + 1) by FINSEQ_1: 39;

 hence thesis by XREAL_1: 6;

 end;

 theorem :: RCOMP_3:47



 Th47: for L be TopSpace, G,G1 be Subset-Family of L st G is Cover of L & G is finite holds for ALL be set st G1 = (G \ { X where X be Subset of L : X in G & ex Y be Subset of L st Y in G & X c< Y }) & ALL = { C where C be Subset-Family of L : C is Cover of L & C c= G1 } holds ALL has_lower_Zorn_property_wrt ( RelIncl ALL)

 proof

 let L be TopSpace;

 let G,G1 be Subset-Family of L;

 assume that

 A1: G is Cover of L and

 A2: G is finite;

 let ALL be set;

 set ZAW = { X where X be Subset of L : X in G & ex Y be Subset of L st Y in G & X c< Y };

 assume that

 A3: G1 = (G \ ZAW) and

 A4: ALL = { C where C be Subset-Family of L : C is Cover of L & C c= G1 };



 A5: G1 is Cover of L by A1, A2, A3, Th45;

 set R = ( RelIncl ALL);



 A6: ( field R) = ALL by WELLORD2:def 1;

 let Y be set such that

 A7: Y c= ALL and

 A8: (R |_2 Y) is being_linear-order;

 per cases ;

 suppose

 A9: Y is non empty;

 defpred A[ set] means $1 is non empty implies ( meet $1) in Y;

 set E = { F(D) where D be Subset-Family of L : D in ( bool G1) };

 take x = ( meet Y);



 A10: ALL c= E

 proof

 let a be object;

 assume a in ALL;

 then ex C be Subset-Family of L st a = C & C is Cover of L & C c= G1 by A4;

 hence thesis;

 end;



 A11: ( bool G1) is finite by A2, A3;

 E is finite from FRAENKEL:sch 21( A11);

 then

 A12: Y is finite by A7, A10;



 A13: for x,B be set st x in Y & B c= Y & A[B] holds A[(B \/ {x})]

 proof

 let x,B be set such that

 A14: x in Y and B c= Y and

 A15: A[B] and (B \/ {x}) is non empty;

 per cases ;

 suppose B is empty;

 hence thesis by A14, SETFAM_1: 10;

 end;

 suppose

 A16: B is non empty;

 (R |_2 Y) is connected by A8;

 then

 A17: (R |_2 Y) is_connected_in ( field (R |_2 Y));

 ( field (R |_2 Y)) = Y by A6, A7, ORDERS_1: 71;

 then [x, ( meet B)] in (R |_2 Y) or [( meet B), x] in (R |_2 Y) or x = ( meet B) by A14, A15, A16, A17;

 then [x, ( meet B)] in R or [( meet B), x] in R or x = ( meet B) by XBOOLE_0:def 4;

 then

 A18: ( meet B) c= x or x c= ( meet B) by A7, A14, A15, A16, WELLORD2:def 1;

 ( meet (B \/ {x})) = (( meet B) /\ ( meet {x})) by A16, SETFAM_1: 9

 .= (( meet B) /\ x) by SETFAM_1: 10;

 hence thesis by A14, A15, A16, A18, XBOOLE_1: 28;

 end;

 end;

 consider y be object such that

 A19: y in Y by A9;

 y in ALL by A7, A19;

 then

 A20: ex C be Subset-Family of L st y = C & C is Cover of L & C c= G1 by A4;

 then

 reconsider X = x as Subset-Family of L by A19, SETFAM_1: 7;



 A21: A[ {} ];



 A22: A[Y] from FINSET_1:sch 2( A12, A21, A13);



 A23: X is Cover of L

 proof

 let a be object;

 assume

 A24: a in the carrier of L;

 ( meet Y) in ALL by A7, A9, A22;

 then

 consider C be Subset-Family of L such that

 A25: ( meet Y) = C and

 A26: C is Cover of L and C c= G1 by A4;

 the carrier of L c= ( union C) by A26, SETFAM_1:def 11;

 hence thesis by A24, A25;

 end;

 x c= G1 by A19, A20, SETFAM_1: 7;

 hence

 A27: x in ALL by A4, A23;

 let y be set;

 assume

 A28: y in Y;

 then x c= y by SETFAM_1: 7;

 hence thesis by A7, A27, A28, WELLORD2:def 1;

 end;

 suppose

 A29: Y is empty;

 take G1;

 thus thesis by A4, A5, A29;

 end;

 end;

 theorem :: RCOMP_3:48



 Th48: for L be TopSpace, G,ALL be set st ALL = { C where C be Subset-Family of L : C is Cover of L & C c= G } holds for M be set st M is_minimal_in ( RelIncl ALL) & M in ( field ( RelIncl ALL)) holds for A1 be Subset of L st A1 in M holds not ex A2,A3 be Subset of L st A2 in M & A3 in M & A1 c= (A2 \/ A3) & A1 <> A2 & A1 <> A3

 proof

 let L be TopSpace;

 let G be set;

 let ALL be set such that

 A1: ALL = { C where C be Subset-Family of L : C is Cover of L & C c= G };

 set R = ( RelIncl ALL);

 let M be set such that

 A2: M is_minimal_in ( RelIncl ALL) and

 A3: M in ( field ( RelIncl ALL));



 A4: ( field R) = ALL by WELLORD2:def 1;

 then

 consider C be Subset-Family of L such that

 A5: M = C and

 A6: C is Cover of L and

 A7: C c= G by A1, A3;

 let A1 be Subset of L such that

 A8: A1 in M;

 set Y = (C \ {A1});



 A9: Y <> M by A8, ZFMISC_1: 56;

 given A2,A3 be Subset of L such that

 A10: A2 in M and

 A11: A3 in M and

 A12: A1 c= (A2 \/ A3) and

 A13: A1 <> A2 and

 A14: A1 <> A3;



 A15: ( union C) = ( [#] L) by A6, SETFAM_1: 45;

 ( union Y) = the carrier of L

 proof

 thus ( union Y) c= the carrier of L;

 let x be object;

 assume

 A16: x in the carrier of L;

 per cases ;

 suppose

 A17: x in A1;

 per cases by A12, A17, XBOOLE_0:def 3;

 suppose

 A18: x in A2;

 A2 in Y by A5, A10, A13, ZFMISC_1: 56;

 hence thesis by A18, TARSKI:def 4;

 end;

 suppose

 A19: x in A3;

 A3 in Y by A5, A11, A14, ZFMISC_1: 56;

 hence thesis by A19, TARSKI:def 4;

 end;

 end;

 suppose

 A20: not x in A1;

 consider Z be set such that

 A21: x in Z and

 A22: Z in C by A15, A16, TARSKI:def 4;

 Z in Y by A20, A21, A22, ZFMISC_1: 56;

 hence thesis by A21, TARSKI:def 4;

 end;

 end;

 then

 A23: Y is Cover of L by SETFAM_1:def 11;



 A24: Y c= M by A5, XBOOLE_1: 36;

 then Y c= G by A5, A7;

 then

 A25: Y in ALL by A1, A23;

 then [Y, M] in R by A4, A3, A24, WELLORD2:def 1;

 hence contradiction by A4, A2, A9, A25;

 end;

 registration

 let X be Subset-Family of REAL ;

 cluster -> real-membered for Element of X;

 coherence

 proof

 let S be Element of X;

 per cases ;

 suppose X is non empty;

 then S in X;

 then S in ( bool REAL );

 then S c= REAL ;

 hence thesis;

 end;

 suppose X is empty;

 then S = {} by SUBSET_1:def 1;

 then S c= REAL ;

 hence thesis;

 end;

 end;

 end

 definition

 let r,s be Real;

 let F be Subset-Family of ( Closed-Interval-TSpace (r,s));

 :: RCOMP_3:def2

 mode IntervalCover of F -> FinSequence of ( bool REAL ) means

 : Def2: ( rng it ) c= F & ( union ( rng it )) = [.r, s.] & (for n be Nat st 1 <= n holds (n <= ( len it ) implies (it /. n) is non empty) & ((n + 1) <= ( len it ) implies ( lower_bound (it /. n)) <= ( lower_bound (it /. (n + 1))) & ( upper_bound (it /. n)) <= ( upper_bound (it /. (n + 1))) & ( lower_bound (it /. (n + 1))) < ( upper_bound (it /. n))) & ((n + 2) <= ( len it ) implies ( upper_bound (it /. n)) <= ( lower_bound (it /. (n + 2))))) & ( [.r, s.] in F implies it = <* [.r, s.]*>) & ( not [.r, s.] in F implies (ex p be Real st r < p & p <= s & (it . 1) = [.r, p.[) & (ex p be Real st r <= p & p < s & (it . ( len it )) = ].p, s.]) & for n be Nat st 1 < n & n < ( len it ) holds ex p,q be Real st r <= p & p < q & q <= s & (it . n) = ].p, q.[);

 existence

 proof

 per cases ;

 suppose

 A5: [.r, s.] in F;

 take f = <* [.r, s.]*>;



 A6: ( rng f) = { [.r, s.]} by FINSEQ_1: 38;

 thus ( rng f) c= F by A5, A6, TARSKI:def 1;

 thus ( union ( rng f)) = [.r, s.] by A6, ZFMISC_1: 25;

 thus thesis by A4, A5, Lm3;

 end;

 suppose

 A7: not [.r, s.] in F;

 set L = ( Closed-Interval-TSpace (r,s));



 A8: the carrier of L = [.r, s.] by A4, TOPMETR: 18;

 A9:

 now

 let A be Subset of L;

 thus A is bounded_above bounded_below by A8, XXREAL_2: 43, XXREAL_2: 44;

 hence A is real-bounded Subset of REAL by A8, XBOOLE_1: 1;

 end;

 L is compact by A4, HEINE: 4;

 then ( [#] L) is compact by COMPTS_1: 1;

 then

 consider G be Subset-Family of L such that

 A10: G c= F and

 A11: G is Cover of ( [#] L) and

 A12: G is finite by A1, A2, COMPTS_1:def 4;

 set ZAW = { X where X be Subset of L : X in G & ex Y be Subset of L st Y in G & X c< Y };

 set G1 = (G \ ZAW);

 set ALL = { C where C be Subset-Family of L : C is Cover of L & C c= G1 };

 set R = ( RelIncl ALL);



 A13: R is_antisymmetric_in ALL by WELLORD2: 21;

 set RM = { ( lower_bound ].c, s.]) where c be Real : ].c, s.] in G1 };

 set LM = { ( upper_bound [.r, b.[) where b be Real : [.r, b.[ in G1 };



 A14: G1 c= G by XBOOLE_1: 36;

 then

 A15: G1 c= F by A10;



 A16: for X be set st X in G1 holds X is interval Subset of REAL

 proof

 let X be set;

 assume X in G1;

 then

 reconsider X as connected Subset of L by A3, A15;

 reconsider Y = X as Subset of REAL by A8, XBOOLE_1: 1;

 Y is interval by Th43;

 hence thesis;

 end;

 reconsider T = L as non empty connected TopSpace by A4, TREAL_1: 20;

 set LM1 = { ( upper_bound E) where E be Subset of L : E in G1 };



 A17: LM c= LM1

 proof

 let x be object;

 assume x in LM;

 then ex b be Real st x = ( upper_bound [.r, b.[) & [.r, b.[ in G1;

 hence thesis;

 end;



 A18: LM c= REAL

 proof

 let x be object;

 assume x in LM;

 then ex b be Real st x = ( upper_bound [.r, b.[) & [.r, b.[ in G1;

 hence thesis by XREAL_0:def 1;

 end;

 set RM1 = { ( lower_bound E) where E be Subset of L : E in G1 };



 A19: RM c= RM1

 proof

 let x be object;

 assume x in RM;

 then ex b be Real st x = ( lower_bound ].b, s.]) & ].b, s.] in G1;

 hence thesis;

 end;



 A20: RM c= REAL

 proof

 let x be object;

 assume x in RM;

 then ex b be Real st x = ( lower_bound ].b, s.]) & ].b, s.] in G1;

 hence thesis by XREAL_0:def 1;

 end;



 A21: ( field R) = ALL by WELLORD2:def 1;

 R is_reflexive_in ALL & R is_transitive_in ALL by WELLORD2: 19, WELLORD2: 20;

 then R partially_orders ALL by A13;

 then

 consider M be set such that

 A22: M is_minimal_in R by A11, A12, A21, Th47, ORDERS_1: 64;



 A23: M in ( field R) by A22;

 then

 consider C be Subset-Family of L such that

 A24: M = C and

 A25: C is Cover of L and

 A26: C c= G1 by A21;



 A27: ( union C) = ( [#] L) by A25, SETFAM_1: 45;



 A28: s in [.r, s.] by A4, XXREAL_1: 1;

 then

 consider R2 be set such that

 A29: s in R2 and

 A30: R2 in C by A8, A27, TARSKI:def 4;

 r in [.r, s.] by A4, XXREAL_1: 1;

 then

 consider R1 be set such that

 A31: r in R1 and

 A32: R1 in C by A8, A27, TARSKI:def 4;



 A33: R1 in G1 by A26, A32;

 then

 A34: R1 in F by A15;



 A35: R2 in G1 by A26, A30;

 then

 A36: R2 in F by A15;

 reconsider R1, R2 as open connected Subset of L by A2, A3, A15, A33, A35;

 A37:

 now

 per cases by A4, A7, A29, A36, Th44;

 suppose ex a be Real st r < a & a <= s & R2 = [.r, a.[;

 hence RM is non empty by A29, XXREAL_1: 3;

 end;

 suppose ex a be Real st r <= a & a < s & R2 = ].a, s.];

 then

 consider a be Real such that r <= a and a < s and

 A38: R2 = ].a, s.];

 ( lower_bound ].a, s.]) in RM by A26, A30, A38;

 hence RM is non empty;

 end;

 suppose ex a,b be Real st r <= a & a < b & b <= s & R2 = ].a, b.[;

 hence RM is non empty by A29, XXREAL_1: 4;

 end;

 end;

 A39:

 now

 per cases by A4, A7, A31, A34, Th44;

 suppose ex a be Real st r < a & a <= s & R1 = [.r, a.[;

 then

 consider a be Real such that r < a and a <= s and

 A40: R1 = [.r, a.[;

 ( upper_bound [.r, a.[) in LM by A26, A32, A40;

 hence LM is non empty;

 end;

 suppose ex a be Real st r <= a & a < s & R1 = ].a, s.];

 hence LM is non empty by A31, XXREAL_1: 2;

 end;

 suppose ex a,b be Real st r <= a & a < b & b <= s & R1 = ].a, b.[;

 hence LM is non empty by A31, XXREAL_1: 4;

 end;

 end;



 A41: G1 is finite by A12;

 RM1 is finite from FRAENKEL:sch 21( A41);

 then

 reconsider RM as non empty finite Subset of REAL by A19, A37, A20;

 F c= ( bool REAL )

 proof

 let a be object;

 reconsider aa = a as set by TARSKI: 1;

 assume a in F;

 then aa c= REAL by A8, XBOOLE_1: 1;

 hence thesis;

 end;

 then G1 c= ( bool REAL ) by A15;

 then

 reconsider X = C as non empty finite Subset-Family of REAL by A12, A26, A32, XBOOLE_1: 1;

 LM1 is finite from FRAENKEL:sch 21( A41);

 then

 reconsider LM as non empty finite Subset of REAL by A17, A39, A18;

 reconsider kL = ( max LM) as Real;

 set LEWY = [.r, kL.[;

 kL in LM by XXREAL_2:def 8;

 then

 consider b be Real such that

 A42: kL = ( upper_bound [.r, b.[) and

 A43: [.r, b.[ in G1;



 A44: ( union G) = ( [#] L) by A11, SETFAM_1: 45;

 A45:

 now

 consider x be object such that

 A46: x in the carrier of L by XBOOLE_0:def 1;

 consider g be set such that

 A47: x in g and

 A48: g in G by A44, A46, TARSKI:def 4;

 {} c= g;

 then

 A49: {} c< g by A47;

 assume

 A50: {} in G1;

 then {} in G by XBOOLE_0:def 5;

 then {} in ZAW by A48, A49;

 hence contradiction by A50, XBOOLE_0:def 5;

 end;

 then

 A51: ( upper_bound LEWY) = kL by A42, A43, Th5, XXREAL_1: 27;



 A52: r < b by A45, A43, XXREAL_1: 27;

 then r < kL by A42, Th5;

 then

 A53: ( lower_bound LEWY) = r by Th4;

 reconsider LEWY as non empty Subset of L by A45, A42, A43, Th5, XXREAL_1: 27;



 A54: kL = b by A45, A42, A43, Th5, XXREAL_1: 27;



 A55: for A be Subset of L st r in A & A in G1 holds A = LEWY

 proof

 let A be Subset of L;

 assume that

 A56: r in A and

 A57: A in G1;



 A58: A in F & A is open by A2, A15, A57;

 A59:

 now

 assume

 A60: (ex a be Real st r <= a & a < s & A = ].a, s.]) or ex a,b be Real st r <= a & a < b & b <= s & A = ].a, b.[;

 per cases by A60;

 suppose ex a be Real st r <= a & a < s & A = ].a, s.];

 hence contradiction by A56, XXREAL_1: 2;

 end;

 suppose ex a,b be Real st r <= a & a < b & b <= s & A = ].a, b.[;

 hence contradiction by A56, XXREAL_1: 4;

 end;

 end;

 A is connected by A3, A15, A57;

 then

 consider ak be Real such that

 A61: r < ak and ak <= s and

 A62: A = [.r, ak.[ by A4, A7, A56, A58, A59, Th44;



 A63: A c= LEWY

 proof

 ( upper_bound A) = ak by A61, A62, Th5;

 then ak in LM by A57, A62;

 then

 A64: ak <= kL by XXREAL_2:def 8;

 let a be object;

 assume

 A65: a in A;

 then a in [.r, s.] by A8;

 then

 reconsider a as Real;

 a < ak by A62, A65, XXREAL_1: 3;

 then

 A66: a < kL by A64, XXREAL_0: 2;

 r <= a by A62, A65, XXREAL_1: 3;

 hence thesis by A66, XXREAL_1: 3;

 end;

 assume A <> LEWY;

 then A c< LEWY by A63;

 then A in ZAW by A14, A43, A54, A57;

 hence contradiction by A57, XBOOLE_0:def 5;

 end;

 then

 reconsider LLEWY = LEWY as Element of X by A26, A31, A32;

 reconsider pP = ( min RM) as Real;

 set PRAWY = ].pP, s.];

 pP in RM by XXREAL_2:def 7;

 then

 consider b be Real such that

 A67: pP = ( lower_bound ].b, s.]) and

 A68: ].b, s.] in G1;



 A69: ( lower_bound PRAWY) = pP by A45, A67, A68, Th6, XXREAL_1: 26;



 A70: b < s by A45, A68, XXREAL_1: 26;

 then pP < s by A67, Th6;

 then

 A71: ( upper_bound PRAWY) = s by Th7;

 reconsider PRAWY as non empty Subset of L by A45, A67, A68, Th6, XXREAL_1: 26;



 A72: pP = b by A45, A67, A68, Th6, XXREAL_1: 26;



 A73: for A be Subset of L st A in G1 & A <> LEWY & A <> PRAWY holds ex a,b be Real st a LEWY and

 A76: A <> PRAWY;



 A77: A in F & A is open connected by A3, A2, A15, A74;

 per cases by A4, A7, A45, A74, A77, Th44;

 suppose ex a be Real st r < a & a <= s & A = [.r, a.[;

 then

 consider a be Real such that r < a and a <= s and

 A78: A = [.r, a.[;

 per cases ;

 suppose a <= kL;

 then A c= LEWY by A78, XXREAL_1: 38;

 then A c< LEWY by A75;

 then A in ZAW by A14, A43, A54, A74;

 hence thesis by A74, XBOOLE_0:def 5;

 end;

 suppose a > kL;

 then LEWY c= A by A78, XXREAL_1: 38;

 then LEWY c< A by A75;

 then LEWY in ZAW by A14, A43, A54, A74;

 hence thesis by A43, A54, XBOOLE_0:def 5;

 end;

 end;

 suppose ex a be Real st r <= a & a < s & A = ].a, s.];

 then

 consider a be Real such that r <= a and a < s and

 A79: A = ].a, s.];

 per cases ;

 suppose a >= pP;

 then A c= PRAWY by A79, XXREAL_1: 42;

 then A c< PRAWY by A76;

 then A in ZAW by A14, A68, A72, A74;

 hence thesis by A74, XBOOLE_0:def 5;

 end;

 suppose a < pP;

 then PRAWY c= A by A79, XXREAL_1: 42;

 then PRAWY c< A by A76;

 then PRAWY in ZAW by A14, A68, A72, A74;

 hence thesis by A68, A72, XBOOLE_0:def 5;

 end;

 end;

 suppose ex a,b be Real st r <= a & a < b & b <= s & A = ].a, b.[;

 then

 consider a,b be Real such that r <= a and

 A80: a < b and b <= s and

 A81: A = ].a, b.[;

 reconsider a, b as Real;

 take a, b;

 thus thesis by A80, A81;

 end;

 end;



 A82: for A be Subset of L st A in G1 & ( upper_bound A) in A holds A = PRAWY

 proof

 let A be Subset of L such that

 A83: A in G1 and

 A84: ( upper_bound A) in A and

 A85: A <> PRAWY;

 A <> LEWY by A51, A84, XXREAL_1: 3;

 then

 consider a,b be Real such that

 A86: a < b and

 A87: A = ].a, b.[ by A73, A83, A85;

 ( upper_bound A) = b by A86, A87, TOPREAL6: 17;

 hence contradiction by A84, A87, XXREAL_1: 4;

 end;

 defpred F[ set, set, set] means ex S be Element of X st S = $2 & ( upper_bound S qua real-membered set) in $3;



 A88: X c= F by A15, A26;



 A89: for Z be Subset of REAL st Z in X holds Z is non empty open connected Subset of T

 proof

 let Z be Subset of REAL ;

 assume

 A90: Z in X;

 then Z is non empty interval by A45, A16, A26;

 hence thesis by A2, A88, A90, Th43;

 end;



 A91: for n be Nat st 1 <= n & n < ( card X) holds for x be Element of X holds ex y be Element of X st F[n, x, y]

 proof

 let n be Nat such that 1 <= n and n < ( card X);

 let x be Element of X;

 reconsider x1 = x as Subset of REAL ;



 A92: x1 is non empty by A89;



 A93: x c= ( union X) by ZFMISC_1: 74;

 then x c= [.r, s.] by A8, A27;

 then x1 is bounded_above by XXREAL_2: 43;

 then ( upper_bound x) is Element of L by A8, A27, A92, A93, Th2;

 then

 consider y be set such that

 A94: ( upper_bound x) in y and

 A95: y in X by A27, TARSKI:def 4;

 reconsider y as Element of X by A95;

 take y, x;

 thus thesis by A94;

 end;

 consider IT be FinSequence of X such that

 A96: ( len IT) = ( card X) and

 A97: (IT . 1) = LLEWY or ( card X) = 0 and

 A98: for n be Nat st 1 <= n & n < ( card X) holds F[n, (IT . n), (IT . (n + 1))] from RECDEF_1:sch 4( A91);



 A99: ( rng IT) c= X;

 ( rng IT) c= ( bool REAL ) by XBOOLE_1: 1;

 then

 reconsider IT as FinSequence of ( bool REAL ) by FINSEQ_1:def 4;



 A100: IT is non empty by A96;

 then

 A101: ( rng IT) is non empty;

 then

 A102: 1 in ( dom IT) by FINSEQ_3: 32;

 then

 A103: (IT /. 1) = (IT . 1) by PARTFUN1:def 6;



 A104: for n be Nat st n in ( dom IT) holds (IT . n) in X & (IT /. n) in X

 proof

 let n be Nat;

 assume n in ( dom IT);

 then (IT . n) = (IT /. n) & (IT . n) in ( rng IT) by FUNCT_1:def 3, PARTFUN1:def 6;

 hence thesis by A99;

 end;



 A105: for n be Nat st n in ( dom IT) holds (IT . n) in G1 & (IT /. n) in G1 by A104, A26;



 A106: for i be Nat st i in ( dom IT) holds for x be Point of L st x < ( upper_bound (IT /. i)) holds ex j be Nat st j in ( dom IT) & j <= i & x in (IT /. j)

 proof

 defpred Q[ Nat] means $1 in ( dom IT) implies for x be Point of L st x < ( upper_bound (IT /. $1)) holds ex j be Nat st j in ( dom IT) & j <= $1 & x in (IT /. j);



 A107: Q[n] implies Q[(n + 1)]

 proof

 assume that

 A108: Q[n] and

 A109: (n + 1) in ( dom IT);



 A110: (IT /. (n + 1)) = (IT . (n + 1)) by A109, PARTFUN1:def 6;

 let x be Point of L such that

 A111: x < ( upper_bound (IT /. (n + 1)));

 per cases by A109, TOPREALA: 2;

 suppose

 A112: n = 0 ;

 take 1;

 thus 1 in ( dom IT) by A101, FINSEQ_3: 32;

 thus 1 <= (n + 1) by A112;

 r <= x by A8, XXREAL_1: 1;

 hence thesis by A51, A97, A111, A110, A112, XXREAL_1: 3;

 end;

 suppose

 A113: n in ( dom IT);

 (n + 1) <= ( len IT) by A109, FINSEQ_3: 25;

 then

 A114: n < ( len IT) by NAT_1: 13;

 1 <= n by A113, FINSEQ_3: 25;

 then

 A115: ex S be Element of X st S = (IT . n) & ( upper_bound S) in (IT . (n + 1)) by A96, A98, A114;

 (IT /. (n + 1)) in X by A104, A109;

 then

 A116: (IT /. (n + 1)) is bounded_below by A9;

 (IT /. n) = (IT . n) by A113, PARTFUN1:def 6;

 then

 A117: ( lower_bound (IT /. (n + 1))) <= ( upper_bound (IT /. n)) by A110, A116, A115, SEQ_4:def 2;



 A118: (IT /. (n + 1)) is interval Subset of REAL & (IT /. (n + 1)) is non empty by A45, A16, A105, A109;

 per cases by XXREAL_0: 1;

 suppose x < ( upper_bound (IT /. n));

 then

 consider j be Nat such that

 A119: j in ( dom IT) and

 A120: j <= n and

 A121: x in (IT /. j) by A108, A113;

 take j;

 thus j in ( dom IT) by A119;

 (j + 0 ) < (n + 1) by A120, XREAL_1: 8;

 hence j <= (n + 1);

 thus thesis by A121;

 end;

 suppose

 A122: x = ( upper_bound (IT /. n));

 take (n + 1);

 thus (n + 1) in ( dom IT) by A109;

 thus (n + 1) <= (n + 1);

 thus thesis by A110, A113, A115, A122, PARTFUN1:def 6;

 end;

 suppose

 A123: x > ( upper_bound (IT /. n));

 take (n + 1);

 thus (n + 1) in ( dom IT) by A109;

 thus (n + 1) <= (n + 1);

 ( lower_bound (IT /. (n + 1))) < x by A117, A123, XXREAL_0: 2;

 hence thesis by A111, A118, Th30;

 end;

 end;

 end;



 A124: Q[ 0 ] by FINSEQ_3: 24;



 A125: Q[n] from NAT_1:sch 2( A124, A107);

 let i be Nat;

 assume i in ( dom IT);

 hence thesis by A125;

 end;



 A126: s in ].b, s.] by A70, XXREAL_1: 2;



 A127: for i be Nat st i in ( dom IT) holds for j be Nat st j in ( dom IT) & i < j holds ex y be Point of L st y in (IT /. j) & for x be Point of L st x in (IT /. i) holds x < y

 proof

 let i be Nat such that

 A128: i in ( dom IT);

 defpred W[ Nat] means $1 in ( dom IT) & i < $1 implies ex y be Point of L st y in (IT /. $1) & for x be Point of L st x in (IT /. i) holds x < y;



 A129: for n holds W[n] implies W[(n + 1)]

 proof

 let n;

 assume that

 A130: W[n] and

 A131: (n + 1) in ( dom IT);



 A132: (IT /. (n + 1)) = (IT . (n + 1)) by A131, PARTFUN1:def 6;

 assume

 A133: i < (n + 1);

 then

 A134: i <= n by NAT_1: 13;

 per cases by A131, TOPREALA: 2;

 suppose n = 0 ;

 then i = 0 by A133, NAT_1: 13;

 hence thesis by A128, FINSEQ_3: 24;

 end;

 suppose

 A135: n in ( dom IT);

 then

 A136: (IT /. n) in X by A104;

 then

 A137: (IT /. n) is bounded_above by A9;



 A138: (IT /. n) = (IT . n) by A135, PARTFUN1:def 6;

 then (IT /. n) in ( rng IT) by A135, FUNCT_1:def 3;

 then

 A139: (IT /. n) is non empty & (IT /. n) is Subset of L by A89, A99;

 then ( upper_bound (IT /. n)) in [.r, s.] by A8, A137, Th2;

 then

 A140: ( upper_bound (IT /. n)) <= s by XXREAL_1: 1;



 A141: (IT /. (n + 1)) in X by A104, A131;



 A142: 1 <= n by A135, FINSEQ_3: 25;



 A143: (IT /. (n + 1)) in ( rng IT) by A131, A132, FUNCT_1:def 3;

 then

 A144: (IT /. (n + 1)) is open connected Subset of L by A89, A99;

 then

 A145: (IT /. (n + 1)) is interval Subset of REAL by Th43;



 A146: (n + 1) <= ( len IT) by A131, FINSEQ_3: 25;

 then n is Element of NAT & n < ( card X) by A96, NAT_1: 13, ORDINAL1:def 12;

 then

 consider S be Element of X such that

 A147: S = (IT . n) and

 A148: ( upper_bound S) in (IT . (n + 1)) by A98, A142;

 (IT /. (n + 1)) is bounded_below by A9, A144;

 then

 A149: ( lower_bound (IT /. (n + 1))) <= ( upper_bound S) by A132, A148, SEQ_4:def 2;



 A150: (IT /. (n + 1)) is bounded_above by A9, A144;

 then

 A151: ( upper_bound S) <= ( upper_bound (IT /. (n + 1))) by A132, A148, SEQ_4:def 1;



 A152: (IT /. (n + 1)) is non empty by A89, A99, A143;

 then ( upper_bound (IT /. (n + 1))) in [.r, s.] by A8, A144, A150, Th2;

 then

 A153: ( upper_bound (IT /. (n + 1))) <= s by XXREAL_1: 1;

 per cases by A134, XXREAL_0: 1;

 suppose i < n;

 then

 consider y be Point of L such that

 A154: y in (IT /. n) and

 A155: for x be Point of L st x in (IT /. i) holds x < y by A130, A135;



 A156: y <= ( upper_bound (IT /. n)) by A137, A154, SEQ_4:def 1;

 per cases by A151, XXREAL_0: 1;

 suppose

 A157: ( upper_bound S) < ( upper_bound (IT /. (n + 1)));

 set y1 = ((( upper_bound S) + ( upper_bound (IT /. (n + 1)))) / 2);



 A158: ( upper_bound S) < y1 by A157, XREAL_1: 226;

 ( upper_bound S) in [.r, s.] by A8, A138, A137, A139, A147, Th2;

 then r <= ( upper_bound S) by XXREAL_1: 1;

 then

 A159: r <= y1 by A158, XXREAL_0: 2;

 y1 < ( upper_bound (IT /. (n + 1))) by A157, XREAL_1: 226;

 then y1 < s by A153, XXREAL_0: 2;

 then

 reconsider y1 as Point of L by A8, A159, XXREAL_1: 1;

 take y1;

 ( lower_bound (IT /. (n + 1))) < y1 by A149, A158, XXREAL_0: 2;

 hence y1 in (IT /. (n + 1)) by A145, A152, A157, Th30, XREAL_1: 226;

 let x be Point of L;

 assume x in (IT /. i);

 then x < ( upper_bound (IT /. n)) by A155, A156, XXREAL_0: 2;

 hence thesis by A138, A147, A158, XXREAL_0: 2;

 end;

 suppose

 A160: ( upper_bound S) = ( upper_bound (IT /. (n + 1)));

 reconsider y1 = s as Point of L by A4, A8, XXREAL_1: 1;

 take y1;

 (IT /. (n + 1)) = PRAWY by A26, A82, A132, A148, A141, A160;

 hence y1 in (IT /. (n + 1)) by A70, A72, XXREAL_1: 2;

 let x be Point of L;

 assume x in (IT /. i);

 then x < ( upper_bound (IT /. n)) by A155, A156, XXREAL_0: 2;

 hence thesis by A140, XXREAL_0: 2;

 end;

 end;

 suppose

 A161: i = n;

 reconsider y1 = ( upper_bound (IT /. n)) as Element of L by A8, A137, A139, Th2;

 take y1;

 thus y1 in (IT /. (n + 1)) by A132, A135, A147, A148, PARTFUN1:def 6;

 let x be Point of L;

 assume

 A162: x in (IT /. i);

 A163:

 now

 set IT1 = (IT | ( Seg n));



 A164: ( rng IT1) c= ( rng IT) by RELAT_1: 70;

 ( rng IT1) c= ( bool the carrier of L)

 proof

 let A be object;

 assume A in ( rng IT1);

 then A in ( rng IT) by A164;

 then A in X by A99;

 hence thesis;

 end;

 then

 reconsider FI = ( rng IT1) as Subset-Family of L;

 assume x = ( upper_bound (IT /. n));

 then

 A165: (IT /. n) = PRAWY by A26, A82, A136, A161, A162;

 A166:

 now

 ( union FI) = the carrier of L

 proof

 thus ( union FI) c= the carrier of L;

 let l be object;

 assume l in the carrier of L;

 then

 reconsider l as Point of L;

 per cases ;

 suppose l < ( upper_bound (IT /. n));

 then

 consider j be Nat such that

 A167: j in ( dom IT) and

 A168: j <= n and

 A169: l in (IT /. j) by A106, A135;

 1 <= j by A167, FINSEQ_3: 25;

 then j in ( Seg n) by A168, FINSEQ_1: 1;

 then

 A170: (IT . j) in FI by A167, FUNCT_1: 50;

 (IT . j) = (IT /. j) by A167, PARTFUN1:def 6;

 hence thesis by A169, A170, TARSKI:def 4;

 end;

 suppose

 A171: l >= ( upper_bound (IT /. n));

 n in ( Seg n) by A142, FINSEQ_1: 1;

 then

 A172: (IT . n) in FI by A135, FUNCT_1: 50;

 l <= s by A8, XXREAL_1: 1;

 then l = s by A71, A165, A171, XXREAL_0: 1;

 hence thesis by A72, A126, A138, A165, A172, TARSKI:def 4;

 end;

 end;

 then

 A173: FI is Cover of L by SETFAM_1:def 11;

 assume

 A174: FI <> X;



 A175: FI c= X by A99, A164;

 then FI c= G1 by A26;

 then

 A176: FI in ALL by A173;

 then [FI, M] in R by A21, A23, A24, A175, WELLORD2:def 1;

 hence contradiction by A21, A22, A24, A174, A176;

 end;

 ( Seg n) c= ( dom IT)

 proof

 let x be object;



 A177: (n + 0 ) <= (n + 1) by XREAL_1: 6;

 assume

 A178: x in ( Seg n);

 then

 reconsider x as Nat;

 x <= n by A178, FINSEQ_1: 1;

 then x <= (n + 1) by A177, XXREAL_0: 2;

 then

 A179: x <= ( len IT) by A146, XXREAL_0: 2;

 1 <= x by A178, FINSEQ_1: 1;

 hence thesis by A179, FINSEQ_3: 25;

 end;

 then ( dom IT1) = ( Seg n) by RELAT_1: 62;

 then ( card ( rng IT1)) <= ( card ( dom IT1)) & ( card ( dom IT1)) = n by CARD_2: 47, FINSEQ_1: 57;

 then (n + 1) <= (n + 0 ) by A96, A146, A166, XXREAL_0: 2;

 hence contradiction by XREAL_1: 6;

 end;

 x <= ( upper_bound (IT /. n)) by A137, A161, A162, SEQ_4:def 1;

 hence thesis by A163, XXREAL_0: 1;

 end;

 end;

 end;



 A180: W[ 0 ];

 for n holds W[n] from NAT_1:sch 2( A180, A129);

 hence thesis;

 end;



 A181: IT is one-to-one

 proof

 let i,j be object such that

 A182: i in ( dom IT) & j in ( dom IT) and

 A183: (IT . i) = (IT . j);



 A184: (IT /. i) = (IT . i) & (IT /. j) = (IT . j) by A182, PARTFUN1:def 6;

 assume

 A185: i <> j;

 reconsider i, j as Nat by A182;

 per cases by A185, XXREAL_0: 1;

 suppose i < j;

 then ex y be Point of L st y in (IT /. j) & for x be Point of L st x in (IT /. i) holds x < y by A127, A182;

 hence thesis by A183, A184;

 end;

 suppose j < i;

 then ex y be Point of L st y in (IT /. i) & for x be Point of L st x in (IT /. j) holds x < y by A127, A182;

 hence thesis by A183, A184;

 end;

 end;



 A186: for i,j be Nat st i in ( dom IT) & j in ( dom IT) & i <> j holds (IT /. i) <> (IT /. j)

 proof

 let i,j be Nat such that

 A187: i in ( dom IT) & j in ( dom IT) and

 A188: i <> j;

 (IT /. i) = (IT . i) & (IT /. j) = (IT . j) by A187, PARTFUN1:def 6;

 hence thesis by A181, A187, A188;

 end;



 A189: for A be Subset of L st s in A & A in G1 holds A = PRAWY

 proof

 let A be Subset of L;

 assume that

 A190: s in A and

 A191: A in G1;



 A192: A in F & A is open by A2, A15, A191;

 A193:

 now

 assume

 A194: (ex a be Real st r < a & a <= s & A = [.r, a.[) or ex a,b be Real st r <= a & a < b & b <= s & A = ].a, b.[;

 per cases by A194;

 suppose ex a be Real st r < a & a <= s & A = [.r, a.[;

 hence contradiction by A190, XXREAL_1: 3;

 end;

 suppose ex a,b be Real st r <= a & a < b & b <= s & A = ].a, b.[;

 hence contradiction by A190, XXREAL_1: 4;

 end;

 end;

 A is connected by A3, A15, A191;

 then

 consider ak be Real such that r <= ak and

 A195: ak < s and

 A196: A = ].ak, s.] by A4, A7, A190, A192, A193, Th44;



 A197: A c= PRAWY

 proof

 ( lower_bound A) = ak by A195, A196, Th6;

 then ak in RM by A191, A196;

 then

 A198: pP <= ak by XXREAL_2:def 7;

 let a be object;

 assume

 A199: a in A;

 then a in [.r, s.] by A8;

 then

 reconsider a as Real;

 ak < a by A196, A199, XXREAL_1: 2;

 then

 A200: pP < a by A198, XXREAL_0: 2;

 a <= s by A196, A199, XXREAL_1: 2;

 hence thesis by A200, XXREAL_1: 2;

 end;

 assume A <> PRAWY;

 then A c< PRAWY by A197;

 then A in ZAW by A14, A68, A72, A191;

 hence contradiction by A191, XBOOLE_0:def 5;

 end;

 take IT;

 thus ( rng IT) c= F by A88, A99;

 ( dom IT) = ( Seg ( len IT)) by FINSEQ_1:def 3;

 then

 A201: ( card ( dom IT)) = ( card X) by A96, FINSEQ_1: 57;

 reconsider IT1 = IT as Function of ( dom IT), X by A99, FUNCT_2: 2;

 IT1 is onto by A201, A181, FINSEQ_4: 63;

 then

 A202: ( rng IT) = X;

 hence ( union ( rng IT)) = [.r, s.] by A8, A27;

 ex Z be set st s in Z & Z in C by A28, A8, A27, TARSKI:def 4;

 then PRAWY in X by A26, A189;

 then

 consider i be object such that

 A203: i in ( dom IT) and

 A204: (IT . i) = PRAWY by A202, FUNCT_1:def 3;

 reconsider i as Element of NAT by A203;



 A205: i <= ( len IT) by A203, FINSEQ_3: 25;



 A206: (IT /. i) = (IT . i) by A203, PARTFUN1:def 6;



 A207: 1 <= i by A203, FINSEQ_3: 25;

 A208:

 now

 assume i <> ( len IT);

 then

 A209: i < ( len IT) by A205, XXREAL_0: 1;

 then

 A210: ex S be Element of X st S = (IT . i) & ( upper_bound S) in (IT . (i + 1)) by A96, A98, A207;

 ( 0 + 1) <= (i + 1) & (i + 1) <= ( len IT) by A209, NAT_1: 13;

 then

 A211: (i + 1) in ( dom IT) by FINSEQ_3: 25;

 then (IT /. (i + 1)) = (IT . (i + 1)) & (IT /. (i + 1)) in G1 by A105, PARTFUN1:def 6;

 then (i + 0 ) = (i + 1) by A71, A189, A186, A203, A204, A206, A210, A211;

 hence contradiction;

 end;



 A212: ( len IT) in ( dom IT) by A100, FINSEQ_5: 6;



 A213: for n be Nat st 1 < n & n < ( len IT) holds ex a,b be Real st r <= a & a < b & b <= s & (IT /. n) = ].a, b.[

 proof

 let n be Nat such that

 A214: 1 < n and

 A215: n < ( len IT);



 A216: n in ( dom IT) by A214, A215, FINSEQ_3: 25;

 then (IT . n) in ( rng IT) by FUNCT_1:def 3;

 then

 A217: (IT /. n) in ( rng IT) by A216, PARTFUN1:def 6;

 then

 A218: (IT /. n) in X by A99;

 then

 A219: (IT /. n) in G1 & (IT /. n) in F by A26, A88;



 A220: (IT /. n) is open connected Subset of L by A89, A99, A217;

 per cases by A4, A7, A45, A219, A220, Th44;

 suppose ex a be Real st r < a & a <= s & (IT /. n) = [.r, a.[;

 then

 consider a be Real such that

 A221: r < a and a <= s and

 A222: (IT /. n) = [.r, a.[;

 r in [.r, a.[ by A221, XXREAL_1: 3;

 hence thesis by A26, A55, A97, A102, A103, A186, A214, A216, A218, A222;

 end;

 suppose ex a be Real st r <= a & a < s & (IT /. n) = ].a, s.];

 then

 consider a be Real such that r <= a and

 A223: a < s and

 A224: (IT /. n) = ].a, s.];

 ( upper_bound ].a, s.]) = s & s in ].a, s.] by A223, Th7, XXREAL_1: 2;

 hence thesis by A26, A82, A212, A186, A204, A206, A208, A215, A216, A218, A224;

 end;

 suppose ex a,b be Real st r <= a & a < b & b <= s & (IT /. n) = ].a, b.[;

 then

 consider a,b be Real such that

 A225: r <= a & a < b & b <= s & (IT /. n) = ].a, b.[;

 reconsider a, b as Real;

 take a, b;

 thus thesis by A225;

 end;

 end;

 A226:

 now

 let n be Nat such that

 A227: 1 <= n;

 reconsider m = n as Element of NAT by ORDINAL1:def 12;

 hereby

 assume n <= ( len IT);

 then m in ( dom IT) & (IT /. n) = (IT . n) by A227, FINSEQ_3: 25, FINSEQ_4: 15;

 then (IT /. n) in ( rng IT) by FUNCT_1:def 3;

 then (IT /. n) in X by A99;

 hence (IT /. n) is non empty by A45, A26;

 end;

 hereby

 assume

 A228: (n + 1) <= ( len IT);

 then

 A229: m < ( len IT) by NAT_1: 13;

 then

 A230: (IT /. n) = (IT . n) by A227, FINSEQ_4: 15;



 A231: m in ( dom IT) by A227, A229, FINSEQ_3: 25;

 then (IT /. n) in ( rng IT) by A230, FUNCT_1:def 3;

 then

 A232: (IT /. n) in X by A99;

 then

 A233: (IT /. n) in G1 by A26;



 A234: (IT /. n) is non empty real-bounded interval Subset of REAL by A9, A45, A16, A26, A232;



 A235: ex S be Element of X st S = (IT . n) & ( upper_bound S) in (IT . (n + 1)) by A96, A98, A227, A229;



 A236: 1 < (m + 1) by A227, NAT_1: 13;

 then

 A237: (IT /. (m + 1)) = (IT . (m + 1)) by A228, FINSEQ_4: 15;



 A238: (n + 1) in ( dom IT) by A228, A236, FINSEQ_3: 25;

 then

 A239: (IT /. (n + 1)) in ( rng IT) by A237, FUNCT_1:def 3;

 then

 A240: (IT /. (n + 1)) in X by A99;

 then

 A241: (IT /. (n + 1)) in G1 by A26;

 (n + 0 ) < (n + 1) by XREAL_1: 6;

 then

 A242: (IT /. n) <> (IT /. (n + 1)) by A186, A231, A238;



 A243: (IT /. (n + 1)) is non empty real-bounded interval Subset of REAL by A9, A45, A16, A26, A240;

 (IT /. (n + 1)) c= ( union X) by A99, A239, ZFMISC_1: 74;

 then (IT /. (n + 1)) c= [.r, s.] by A8, A27;

 then

 A244: (IT /. (n + 1)) is bounded_above by XXREAL_2: 43;

 then

 A245: ( upper_bound (IT /. n)) <= ( upper_bound (IT /. (n + 1))) by A235, A230, A237, SEQ_4:def 1;

 hereby

 assume

 A246: ( lower_bound (IT /. n)) > ( lower_bound (IT /. (n + 1)));

 ( upper_bound (IT /. (n + 1))) = ( upper_bound (IT /. n)) & ( upper_bound (IT /. n)) in (IT /. n) implies ( upper_bound (IT /. (n + 1))) in (IT /. (n + 1)) by A26, A82, A212, A186, A204, A206, A208, A229, A231, A232;

 then (IT /. n) c= (IT /. (n + 1)) by A234, A243, A245, A246, Th31;

 then (IT /. n) c< (IT /. (n + 1)) by A242;

 then (IT /. n) in ZAW by A14, A233, A241;

 hence contradiction by A26, A232, XBOOLE_0:def 5;

 end;

 thus ( upper_bound (IT /. n)) <= ( upper_bound (IT /. (n + 1))) by A235, A230, A237, A244, SEQ_4:def 1;

 per cases by A228, XXREAL_0: 1;

 suppose

 A247: (n + 1) = ( len IT);

 then pP < ( upper_bound (IT /. n)) by A204, A208, A235, A230, XXREAL_1: 2;

 hence ( lower_bound (IT /. (n + 1))) < ( upper_bound (IT /. n)) by A204, A206, A208, A247, Th6, XXREAL_1: 26;

 end;

 suppose (n + 1) < ( len IT);

 then

 consider a1,b1 be Real such that r <= a1 and

 A248: a1 < b1 and b1 <= s and

 A249: (IT /. (n + 1)) = ].a1, b1.[ by A213, A236;

 a1 < ( upper_bound (IT /. n)) by A235, A230, A237, A249, XXREAL_1: 4;

 hence ( lower_bound (IT /. (n + 1))) < ( upper_bound (IT /. n)) by A248, A249, TOPREAL6: 17;

 end;

 end;

 end;

 hereby

 let n be Nat such that

 A250: 1 <= n;

 thus

 A251: (n <= ( len IT) implies (IT /. n) is non empty) & ((n + 1) <= ( len IT) implies ( lower_bound (IT /. n)) <= ( lower_bound (IT /. (n + 1))) & ( upper_bound (IT /. n)) <= ( upper_bound (IT /. (n + 1))) & ( lower_bound (IT /. (n + 1))) < ( upper_bound (IT /. n))) by A226, A250;

 reconsider m = n as Nat;



 A252: (n + 0 ) < (n + 1) by XREAL_1: 6;

 then

 A253: 1 < (m + 1) by A250, XXREAL_0: 2;

 assume

 A254: (n + 2) <= ( len IT);

 then

 A255: ((n + 1) + 1) <= ( len IT);

 then

 A256: (m + 1) < ( len IT) by NAT_1: 13;

 then

 A257: (n + 1) in ( dom IT) by A253, FINSEQ_3: 25;

 then (IT /. (n + 1)) = (IT . (n + 1)) by PARTFUN1:def 6;

 then (IT /. (n + 1)) in ( rng IT) by A257, FUNCT_1:def 3;

 then

 A258: (IT /. (n + 1)) in X by A99;

 ( 0 + 1) <= (n + 1) by XREAL_1: 6;

 then

 A259: ( upper_bound (IT /. (n + 1))) <= ( upper_bound (IT /. ((n + 1) + 1))) by A226, A254;

 assume

 A260: ( upper_bound (IT /. n)) > ( lower_bound (IT /. (n + 2)));

 consider a1,b1 be Real such that r <= a1 and

 A261: a1 < b1 and b1 <= s and

 A262: (IT /. (n + 1)) = ].a1, b1.[ by A213, A253, A256;



 A263: ( lower_bound ].a1, b1.[) = a1 by A261, TOPREAL6: 17;



 A264: ( upper_bound ].a1, b1.[) = b1 by A261, TOPREAL6: 17;



 A265: (IT /. (n + 1)) c= ((IT /. n) \/ (IT /. (n + 2)))

 proof

 let x be object;

 assume

 A266: x in (IT /. (n + 1));

 then

 reconsider x as Real;



 A267: a1 < x by A262, A266, XXREAL_1: 4;



 A268: x < b1 by A262, A266, XXREAL_1: 4;

 per cases ;

 suppose

 A269: x < ( upper_bound (IT /. n));

 per cases ;

 suppose

 A270: n = 1;

 then ( lower_bound (IT /. n)) <= x by A8, A53, A97, A103, A258, A266, XXREAL_1: 1;

 then x in (IT /. n) by A42, A54, A53, A97, A103, A269, A270, XXREAL_1: 3;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose

 A271: n <> 1;

 (n + 0 ) < (n + 2) by XREAL_1: 6;

 then

 A272: n < ( len IT) by A254, XXREAL_0: 2;



 A273: ( lower_bound (IT /. n)) < x by A251, A255, A262, A263, A267, NAT_1: 13, XXREAL_0: 2;

 1 < n by A250, A271, XXREAL_0: 1;

 then

 consider a,b be Real such that r <= a and

 A274: a < b and b <= s and

 A275: (IT /. n) = ].a, b.[ by A213, A272;

 ( lower_bound (IT /. n)) = a & ( upper_bound (IT /. n)) = b by A274, A275, TOPREAL6: 17;

 then x in (IT /. n) by A269, A275, A273, XXREAL_1: 4;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 suppose x >= ( upper_bound (IT /. n));

 then

 A276: x > ( lower_bound (IT /. (n + 2))) by A260, XXREAL_0: 2;

 per cases ;

 suppose

 A277: ( len IT) = (n + 2);

 x <= s by A8, A258, A266, XXREAL_1: 1;

 then x in (IT /. (n + 2)) by A69, A204, A206, A208, A276, A277, XXREAL_1: 2;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose

 A278: ( len IT) <> (n + 2);

 (n + 1) < (n + 2) by XREAL_1: 6;

 then

 A279: 1 < (n + 2) by A253, XXREAL_0: 2;

 ((n + 1) + 1) < ( len IT) by A254, A278, XXREAL_0: 1;

 then

 consider a2,b2 be Real such that r <= a2 and

 A280: a2 < b2 and b2 <= s and

 A281: (IT /. (n + 2)) = ].a2, b2.[ by A213, A279;

 ( upper_bound ].a2, b2.[) = b2 by A280, TOPREAL6: 17;

 then

 A282: x < b2 by A259, A262, A264, A268, A281, XXREAL_0: 2;

 ( lower_bound ].a2, b2.[) = a2 by A280, TOPREAL6: 17;

 then x in (IT /. (n + 2)) by A276, A281, A282, XXREAL_1: 4;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 end;

 (m + 1) <= (m + 2) by XREAL_1: 6;

 then 1 <= (m + 2) by A253, XXREAL_0: 2;

 then

 A283: (m + 2) in ( dom IT) by A254, FINSEQ_3: 25;

 then (IT /. (n + 2)) = (IT . (n + 2)) by PARTFUN1:def 6;

 then (IT /. (n + 2)) in ( rng IT) by A283, FUNCT_1:def 3;

 then

 A284: (IT /. (n + 2)) in X by A99;

 m <= ( len IT) by A252, A256, XXREAL_0: 2;

 then

 A285: n in ( dom IT) by A250, FINSEQ_3: 25;

 then (IT /. n) = (IT . n) by PARTFUN1:def 6;

 then (IT /. n) in ( rng IT) by A285, FUNCT_1:def 3;

 then

 A286: (IT /. n) in X by A99;

 (n + 1) < (n + 2) by XREAL_1: 6;

 then

 A287: (IT /. (n + 2)) <> (IT /. (n + 1)) by A186, A257, A283;

 (n + 0 ) < (n + 1) by XREAL_1: 6;

 then (IT /. n) <> (IT /. (n + 1)) by A186, A285, A257;

 hence contradiction by A22, A24, A286, A258, A284, A287, A265, Th48;

 end;

 thus [.r, s.] in F implies IT = <* [.r, s.]*> by A7;

 assume not [.r, s.] in F;

 thus ex p be Real st r < p & p <= s & (IT . 1) = [.r, p.[

 proof

 take kL;

 thus r < kL by A42, A52, Th5;

 ( upper_bound LEWY) <= ( upper_bound [.r, s.]) by A8, SEQ_4: 48;

 hence kL <= s by A4, A51, JORDAN5A: 19;

 thus thesis by A97;

 end;

 thus ex p be Real st r <= p & p < s & (IT . ( len IT)) = ].p, s.]

 proof

 take pP;

 ( lower_bound [.r, s.]) <= ( lower_bound PRAWY) by A8, SEQ_4: 47;

 hence r <= pP by A4, A69, JORDAN5A: 19;

 thus pP < s by A67, A70, Th6;

 thus thesis by A204, A208;

 end;

 let n be Nat such that

 A288: 1 < n & n < ( len IT);

 consider a,b be Real such that

 A289: r <= a & a < b & b <= s & (IT /. n) = ].a, b.[ by A213, A288;

 take a, b;

 thus thesis by A288, A289, FINSEQ_4: 15;

 end;

 end;

 end

 theorem :: RCOMP_3:49

 F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & [.r, s.] in F implies <* [.r, s.]*> is IntervalCover of F

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected and

 A2: r <= s & [.r, s.] in F;

 set f = <* [.r, s.]*>;



 A3: for n be Nat st 1 <= n holds (n <= ( len f) implies (f /. n) is non empty) & ((n + 1) <= ( len f) implies ( lower_bound (f /. n)) <= ( lower_bound (f /. (n + 1))) & ( upper_bound (f /. n)) <= ( upper_bound (f /. (n + 1))) & ( lower_bound (f /. (n + 1))) < ( upper_bound (f /. n))) & ((n + 2) <= ( len f) implies ( upper_bound (f /. n)) <= ( lower_bound (f /. (n + 2)))) by A2, Lm3;

 ( rng f) c= F & ( union ( rng f)) = [.r, s.] by A2, Lm3;

 hence thesis by A1, A2, A3, Def2;

 end;

 reserve C for IntervalCover of F;

 theorem :: RCOMP_3:50



 Th50: for F be Subset-Family of ( Closed-Interval-TSpace (r,r)), C be IntervalCover of F holds F is Cover of ( Closed-Interval-TSpace (r,r)) & F is open connected implies C = <* [.r, r.]*>

 proof

 set L = ( Closed-Interval-TSpace (r,r));

 let F be Subset-Family of L, C be IntervalCover of F;

 assume that

 A1: F is Cover of L and

 A2: F is open & F is connected;



 A3: [.r, r.] = {r} by XXREAL_1: 17;

 the carrier of L = [.r, r.] by TOPMETR: 18;

 then r in the carrier of L by A3, TARSKI:def 1;

 then {r} in F by A1, Th46;

 hence thesis by A1, A2, A3, Def2;

 end;

 theorem :: RCOMP_3:51



 Th51: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s implies 1 <= ( len C)

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected and

 A2: r <= s;

 assume not thesis;

 then (( len C) + 1) <= ( 0 + 1) by NAT_1: 13;

 then

 A3: C is empty by XREAL_1: 6;

 ( union ( rng C)) = [.r, s.] by A1, A2, Def2;

 hence thesis by A2, A3, RELAT_1: 38, XXREAL_1: 1, ZFMISC_1: 2;

 end;

 theorem :: RCOMP_3:52



 Th52: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & ( len C) = 1 implies C = <* [.r, s.]*>

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s and

 A2: ( len C) = 1;



 A3: ( union ( rng C)) = [.r, s.] by A1, Def2;

 C is non empty by A2;

 then ( rng C) is non empty;

 then 1 in ( dom C) by FINSEQ_3: 32;

 then

 A4: (C . 1) in ( rng C) by FUNCT_1:def 3;

 (C . 1) = [.r, s.]

 proof

 thus for a be object st a in (C . 1) holds a in [.r, s.] by A3, A4, TARSKI:def 4;

 let a be object;



 A5: ( dom C) = {1} by A2, FINSEQ_1: 2, FINSEQ_1:def 3;

 assume a in [.r, s.];

 then

 consider Z be set such that

 A6: a in Z and

 A7: Z in ( rng C) by A3, TARSKI:def 4;

 ex x be object st x in ( dom C) & (C . x) = Z by A7, FUNCT_1:def 3;

 hence thesis by A6, A5, TARSKI:def 1;

 end;

 hence thesis by A2, FINSEQ_1: 40;

 end;

 theorem :: RCOMP_3:53

 F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & n in ( dom C) & m in ( dom C) & n < m implies ( lower_bound (C /. n)) <= ( lower_bound (C /. m))

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s and

 A2: n in ( dom C) and

 A3: m in ( dom C) & n < m;

 defpred P[ Nat] means $1 in ( dom C) & n < $1 implies ( lower_bound (C /. n)) <= ( lower_bound (C /. $1));



 A4: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A5: P[k] and

 A6: (k + 1) in ( dom C) and

 A7: n < (k + 1);

 per cases by A6, TOPREALA: 2;

 suppose k = 0 ;

 then n = 0 by A7, NAT_1: 13;

 hence thesis by A2, FINSEQ_3: 24;

 end;

 suppose

 A8: k in ( dom C);



 A9: (k + 1) <= ( len C) by A6, FINSEQ_3: 25;



 A10: n <= k by A7, NAT_1: 13;

 1 <= k by A8, FINSEQ_3: 25;

 then ( lower_bound (C /. k)) <= ( lower_bound (C /. (k + 1))) by A1, A9, Def2;

 hence thesis by A5, A8, A10, XXREAL_0: 1, XXREAL_0: 2;

 end;

 end;



 A11: P[ 0 ];

 for k be Nat holds P[k] from NAT_1:sch 2( A11, A4);

 hence thesis by A3;

 end;

 theorem :: RCOMP_3:54

 F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & n in ( dom C) & m in ( dom C) & n < m implies ( upper_bound (C /. n)) <= ( upper_bound (C /. m))

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s and

 A2: n in ( dom C) and

 A3: m in ( dom C) & n < m;

 defpred P[ Nat] means $1 in ( dom C) & n < $1 implies ( upper_bound (C /. n)) <= ( upper_bound (C /. $1));



 A4: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A5: P[k] and

 A6: (k + 1) in ( dom C) and

 A7: n < (k + 1);

 per cases by A6, TOPREALA: 2;

 suppose k = 0 ;

 then n = 0 by A7, NAT_1: 13;

 hence thesis by A2, FINSEQ_3: 24;

 end;

 suppose

 A8: k in ( dom C);



 A9: (k + 1) <= ( len C) by A6, FINSEQ_3: 25;



 A10: n <= k by A7, NAT_1: 13;

 1 <= k by A8, FINSEQ_3: 25;

 then ( upper_bound (C /. k)) <= ( upper_bound (C /. (k + 1))) by A1, A9, Def2;

 hence thesis by A5, A8, A10, XXREAL_0: 1, XXREAL_0: 2;

 end;

 end;



 A11: P[ 0 ];

 for k be Nat holds P[k] from NAT_1:sch 2( A11, A4);

 hence thesis by A3;

 end;

 theorem :: RCOMP_3:55



 Th55: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & 1 <= n & (n + 1) <= ( len C) implies ].( lower_bound (C /. (n + 1))), ( upper_bound (C /. n)).[ is non empty

 proof

 assume F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & (n + 1) <= ( len C);

 then ( lower_bound (C /. (n + 1))) < ( upper_bound (C /. n)) by Def2;

 hence thesis by XXREAL_1: 33;

 end;

 theorem :: RCOMP_3:56

 F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s implies ( lower_bound (C /. 1)) = r

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected and

 A2: r <= s;

 1 <= ( len C) by A1, A2, Th51;

 then

 A3: (C . 1) = (C /. 1) by FINSEQ_4: 15;

 per cases ;

 suppose [.r, s.] in F;

 then C = <* [.r, s.]*> by A1, A2, Def2;

 then (C /. 1) = [.r, s.] by FINSEQ_4: 16;

 hence thesis by A2, JORDAN5A: 19;

 end;

 suppose not [.r, s.] in F;

 then ex p be Real st r < p & p <= s & (C . 1) = [.r, p.[ by A1, A2, Def2;

 hence thesis by A3, Th4;

 end;

 end;

 theorem :: RCOMP_3:57



 Th57: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s implies r in (C /. 1)

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected and

 A2: r <= s;

 1 <= ( len C) by A1, A2, Th51;

 then

 A3: (C . 1) = (C /. 1) by FINSEQ_4: 15;

 per cases ;

 suppose [.r, s.] in F;

 then C = <* [.r, s.]*> by A1, A2, Def2;

 then (C /. 1) = [.r, s.] by FINSEQ_4: 16;

 hence thesis by A2, XXREAL_1: 1;

 end;

 suppose not [.r, s.] in F;

 then ex p be Real st r < p & p <= s & (C . 1) = [.r, p.[ by A1, A2, Def2;

 hence thesis by A3, XXREAL_1: 3;

 end;

 end;

 theorem :: RCOMP_3:58

 F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s implies ( upper_bound (C /. ( len C))) = s

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected and

 A2: r <= s;

 1 <= ( len C) by A1, A2, Th51;

 then

 A3: (C . ( len C)) = (C /. ( len C)) by FINSEQ_4: 15;

 per cases ;

 suppose [.r, s.] in F;

 then C = <* [.r, s.]*> by A1, A2, Def2;

 then (C /. 1) = [.r, s.] & ( len C) = 1 by FINSEQ_1: 39, FINSEQ_4: 16;

 hence thesis by A2, JORDAN5A: 19;

 end;

 suppose not [.r, s.] in F;

 then ex p be Real st r <= p & p < s & (C . ( len C)) = ].p, s.] by A1, A2, Def2;

 hence thesis by A3, Th7;

 end;

 end;

 theorem :: RCOMP_3:59



 Th59: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s implies s in (C /. ( len C))

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected and

 A2: r <= s;

 1 <= ( len C) by A1, A2, Th51;

 then

 A3: (C . ( len C)) = (C /. ( len C)) by FINSEQ_4: 15;

 per cases ;

 suppose [.r, s.] in F;

 then C = <* [.r, s.]*> by A1, A2, Def2;

 then (C /. 1) = [.r, s.] & ( len C) = 1 by FINSEQ_1: 39, FINSEQ_4: 16;

 hence thesis by A2, XXREAL_1: 1;

 end;

 suppose not [.r, s.] in F;

 then ex p be Real st r <= p & p < s & (C . ( len C)) = ].p, s.] by A1, A2, Def2;

 hence thesis by A3, XXREAL_1: 2;

 end;

 end;

 definition

 let r,s be Real;

 let F be Subset-Family of ( Closed-Interval-TSpace (r,s)), C be IntervalCover of F;

 :: RCOMP_3:def3

 mode IntervalCoverPts of C -> FinSequence of REAL means

 : Def3: ( len it ) = (( len C) + 1) & (it . 1) = r & (it . ( len it )) = s & for n be Nat st 1 <= n & (n + 1) < ( len it ) holds (it . (n + 1)) in ].( lower_bound (C /. (n + 1))), ( upper_bound (C /. n)).[;

 existence

 proof

 set A = (( len C) + 1);

 defpred P[ Nat, set] means ($1 = 1 implies $2 = r) & ($1 = A implies $2 = s) & (2 <= $1 & $1 <= ( len C) implies $2 in ].( lower_bound (C /. $1)), ( upper_bound (C /. ($1 - 1))).[);



 A2: ( 0 + 1) <= ( len C) by A1, Th51;

 then

 A3: ( 0 + 1) < A by XREAL_1: 6;



 A4: for k be Nat st k in ( Seg A) holds ex x be Element of REAL st P[k, x]

 proof

 reconsider r, s as Element of REAL by XREAL_0:def 1;

 let k be Nat;



 A5: (( len C) + 0 ) < A by XREAL_1: 6;

 assume k in ( Seg A);

 then

 A6: 1 <= k & k <= A by FINSEQ_1: 1;

 per cases by A6, XXREAL_0: 1;

 suppose

 A7: k = 1;

 take r;

 thus thesis by A2, A7;

 end;

 suppose

 A8: k = A;

 take s;

 thus thesis by A2, A5, A8;

 end;

 suppose that

 A9: 1 < k and

 A10: k < A;



 A11: (k - 1) in NAT by A9, INT_1: 5;



 A12: k <= ( len C) by A10, NAT_1: 13;

 (1 - 1) < (k - 1) by A9, XREAL_1: 14;

 then ( 0 + 1) <= (k - 1) by A11, NAT_1: 13;

 then ].( lower_bound (C /. ((k - 1) + 1))), ( upper_bound (C /. (k - 1))).[ is non empty by A1, A11, A12, Th55;

 then

 consider x be object such that

 A13: x in ].( lower_bound (C /. ((k - 1) + 1))), ( upper_bound (C /. (k - 1))).[;

 reconsider x as Real by A13;

 take x;

 thus thesis by A9, A10, A13;

 end;

 end;

 consider p be FinSequence of REAL such that

 A14: ( dom p) = ( Seg A) and

 A15: for k be Nat st k in ( Seg A) holds P[k, (p . k)] from FINSEQ_1:sch 5( A4);

 take p;

 thus

 A16: ( len p) = (( len C) + 1) by A14, FINSEQ_1:def 3;

 1 in ( Seg A) by A3, FINSEQ_1: 1;

 hence (p . 1) = r by A15;

 ( len p) in ( Seg A) by A3, A16, FINSEQ_1: 1;

 hence (p . ( len p)) = s by A15, A16;

 let n be Nat;

 assume 1 <= n;

 then

 A17: (1 + 1) <= (n + 1) by XREAL_1: 6;

 assume

 A18: (n + 1) < ( len p);

 ( 0 + 1) <= (n + 1) by XREAL_1: 6;

 then

 A19: (n + 1) in ( Seg A) by A16, A18, FINSEQ_1: 1;

 (n + 1) <= ( len C) by A16, A18, NAT_1: 13;

 then (p . (n + 1)) in ].( lower_bound (C /. (n + 1))), ( upper_bound (C /. ((n + 1) - 1))).[ by A15, A19, A17;

 hence thesis;

 end;

 end

 reserve G for IntervalCoverPts of C;

 theorem :: RCOMP_3:60



 Th60: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s implies 2 <= ( len G)

 proof

 assume

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s;

 then 1 <= ( len C) by Th51;

 then (1 + 1) <= (( len C) + 1) by XREAL_1: 6;

 hence thesis by A1, Def3;

 end;

 theorem :: RCOMP_3:61



 Th61: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & ( len C) = 1 implies G = <*r, s*>

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s and

 A2: ( len C) = 1;



 A3: (G . 1) = r by A1, Def3;



 A4: ( len G) = (( len C) + 1) by A1, Def3;

 then (G . 2) = s by A1, A2, Def3;

 hence thesis by A2, A4, A3, FINSEQ_1: 44;

 end;

 theorem :: RCOMP_3:62



 Th62: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & 1 <= n & (n + 1) < ( len G) implies (G . (n + 1)) < ( upper_bound (C /. n))

 proof

 assume F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & (n + 1) < ( len G);

 then (G . (n + 1)) in ].( lower_bound (C /. (n + 1))), ( upper_bound (C /. n)).[ by Def3;

 hence thesis by XXREAL_1: 4;

 end;

 theorem :: RCOMP_3:63



 Th63: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & 1 < n & n <= ( len C) implies ( lower_bound (C /. n)) < (G . n)

 proof

 set w = (n -' 1);

 assume

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s;

 then

 A2: ( len G) = (( len C) + 1) by Def3;

 assume that

 A3: 1 < n and

 A4: n <= ( len C);



 A5: n < (( len C) + 1) by A4, NAT_1: 13;

 (1 - 1) <= (n - 1) by A3, XREAL_1: 9;

 then

 A6: w = (n - 1) by XREAL_0:def 2;

 then n = (w + 1);

 then 1 <= w by A3, NAT_1: 13;

 then (G . (w + 1)) in ].( lower_bound (C /. (w + 1))), ( upper_bound (C /. w)).[ by A1, A2, A6, A5, Def3;

 hence thesis by A6, XXREAL_1: 4;

 end;

 theorem :: RCOMP_3:64



 Th64: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & 1 <= n & n < ( len C) implies (G . n) <= ( lower_bound (C /. (n + 1)))

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected and

 A2: r <= s;

 set w = (n -' 1);

 assume that

 A3: 1 <= n and

 A4: n < ( len C);



 A5: (n + 1) <= ( len C) by A4, NAT_1: 13;

 per cases by A3, XXREAL_0: 1;

 suppose

 A6: n = 1;

 ( 0 + 1) <= (n + 1) by XREAL_1: 6;

 then

 A7: (C /. (n + 1)) is non empty by A1, A2, A5, Def2;



 A8: (G . 1) = r by A1, A2, Def3;



 A9: ( rng C) c= F by A1, A2, Def2;

 (1 + 1) <= ( len C) by A4, A6, NAT_1: 13;

 then

 A10: 2 in ( dom C) by FINSEQ_3: 25;

 then (C . 2) in ( rng C) by FUNCT_1:def 3;

 then (C . 2) in F by A9;

 then (C /. 2) in F by A10, PARTFUN1:def 6;

 then (C /. (n + 1)) c= the carrier of ( Closed-Interval-TSpace (r,s)) by A6;

 then

 A11: (C /. (n + 1)) c= [.r, s.] by A2, TOPMETR: 18;

 then (C /. (n + 1)) is bounded_below by XXREAL_2: 44;

 then ( lower_bound (C /. (n + 1))) in [.r, s.] by A7, A11, Th1;

 hence thesis by A6, A8, XXREAL_1: 1;

 end;

 suppose 1 < n;

 then

 A12: (1 - 1) < (n - 1) by XREAL_1: 9;

 then

 A13: w = (n - 1) by XREAL_0:def 2;

 then

 A14: ( 0 + 1) <= w by A12, NAT_1: 13;

 ( len G) = (( len C) + 1) by A1, A2, Def3;

 then

 A15: (n + 1) < ((( len G) - 1) + 1) by A4, XREAL_1: 6;

 (n - 1) < (n - 0 ) by XREAL_1: 15;

 then (w + 1) < (n + 1) by A13, XREAL_1: 6;

 then (w + 1) < ( len G) by A15, XXREAL_0: 2;

 then

 A16: (G . (w + 1)) < ( upper_bound (C /. w)) by A1, A2, A14, Th62;

 (n + 1) <= ( len C) by A4, NAT_1: 13;

 then ( upper_bound (C /. w)) <= ( lower_bound (C /. (w + 2))) by A1, A2, A13, A14, Def2;

 hence thesis by A13, A16, XXREAL_0: 2;

 end;

 end;

 theorem :: RCOMP_3:65



 Th65: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r < s implies G is increasing

 proof

 assume that

 A1: F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open & F is connected and

 A2: r < s;

 let m,n be Nat such that

 A3: m in ( dom G) & n in ( dom G) & m < n;

 defpred P[ Nat] means m < $1 & m in ( dom G) & $1 in ( dom G) implies (G . m) < (G . $1);



 A4: for k be Nat st P[k] holds P[(k + 1)]

 proof



 A5: ( len G) = (( len C) + 1) by A1, A2, Def3;

 let k be Nat such that

 A6: P[k] and

 A7: m < (k + 1) and

 A8: m in ( dom G) and

 A9: (k + 1) in ( dom G);



 A10: 1 <= m by A8, FINSEQ_3: 25;



 A11: (k + 1) <= ( len G) by A9, FINSEQ_3: 25;

 (k + 0 ) <= (k + 1) by XREAL_1: 6;

 then

 A12: k <= ( len G) by A11, XXREAL_0: 2;



 A13: m <= k by A7, NAT_1: 13;

 then

 A14: 1 <= k by A10, XXREAL_0: 2;

 per cases by A14, A11, XXREAL_0: 1;

 suppose that

 A15: 1 < k and

 A16: (k + 1) < ( len G);

 (G . (k + 1)) in ].( lower_bound (C /. (k + 1))), ( upper_bound (C /. k)).[ by A1, A2, A15, A16, Def3;

 then

 A17: ( lower_bound (C /. (k + 1))) < (G . (k + 1)) by XXREAL_1: 4;

 k < ( len C) by A5, A16, XREAL_1: 6;

 then (G . k) <= ( lower_bound (C /. (k + 1))) by A1, A2, A15, Th64;

 then (G . k) < (G . (k + 1)) by A17, XXREAL_0: 2;

 hence thesis by A6, A8, A13, A12, A15, FINSEQ_3: 25, XXREAL_0: 1, XXREAL_0: 2;

 end;

 suppose

 A18: k = 1;



 A19: 1 <= ( len C) by A1, A2, Th51;



 A20: m <= 1 by A7, A18, NAT_1: 13;

 per cases by A19, XXREAL_0: 1;

 suppose

 A21: 1 < ( len C);

 then (1 + 1) <= ( len C) by NAT_1: 13;

 then

 A22: ( lower_bound (C /. 2)) < (G . 2) by A1, A2, Th63;

 (G . 1) <= ( lower_bound (C /. (1 + 1))) by A1, A2, A21, Th64;

 then (G . 1) < (G . 2) by A22, XXREAL_0: 2;

 hence thesis by A10, A18, A20, XXREAL_0: 1;

 end;

 suppose 1 = ( len C);

 then G = <*r, s*> by A1, A2, Th61;

 then (G . 1) = r & (G . 2) = s by FINSEQ_1: 44;

 hence thesis by A2, A10, A18, A20, XXREAL_0: 1;

 end;

 end;

 suppose

 A23: (k + 1) = ( len G);

 then

 A24: (G . (k + 1)) = s by A1, A2, Def3;

 per cases by A10, XXREAL_0: 1;

 suppose

 A25: 1 < m;

 set z = (m -' 1);

 (1 - 1) <= (m - 1) by A10, XREAL_1: 9;

 then

 A26: z = (m - 1) by XREAL_0:def 2;

 then

 A27: (z + 1) < ( len G) by A7, A23;

 then

 A28: z <= ( len C) by A5, XREAL_1: 6;

 (1 + 1) <= m by A25, NAT_1: 13;

 then

 A29: ((1 + 1) - 1) <= (m - 1) by XREAL_1: 9;

 then

 A30: 1 <= z by XREAL_0:def 2;

 then

 A31: (C /. z) is non empty by A1, A2, A28, Def2;



 A32: ( rng C) c= F by A1, A2, Def2;



 A33: z in ( dom C) by A30, A28, FINSEQ_3: 25;

 then (C . z) in ( rng C) by FUNCT_1:def 3;

 then (C . z) in F by A32;

 then (C /. z) in F by A33, PARTFUN1:def 6;

 then (C /. z) c= the carrier of ( Closed-Interval-TSpace (r,s));

 then

 A34: (C /. z) c= [.r, s.] by A2, TOPMETR: 18;

 then (C /. z) is bounded_above by XXREAL_2: 43;

 then ( upper_bound (C /. z)) in [.r, s.] by A34, A31, Th2;

 then

 A35: ( upper_bound (C /. z)) <= s by XXREAL_1: 1;

 (G . m) < ( upper_bound (C /. z)) by A1, A2, A26, A29, A27, Th62;

 hence thesis by A24, A35, XXREAL_0: 2;

 end;

 suppose m = 1;

 hence thesis by A1, A2, A24, Def3;

 end;

 end;

 end;



 A36: P[ 0 ];

 for k be Nat holds P[k] from NAT_1:sch 2( A36, A4);

 hence thesis by A3;

 end;

 theorem :: RCOMP_3:66

 F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s & 1 <= n & n < ( len G) implies [.(G . n), (G . (n + 1)).] c= (C . n)

 proof

 set L = ( Closed-Interval-TSpace (r,s));

 assume that

 A1: F is Cover of L & F is open and

 A2: F is connected and

 A3: r <= s and

 A4: 1 <= n and

 A5: n < ( len G);



 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 L by A2;

 then

 A10: (C /. n) is interval by Th43;



 A11: (C /. n) is non 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 by A3, XXREAL_0: 1;

 suppose r = s;

 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 thesis by A17, FINSEQ_1: 40;

 end;

 suppose r < s;

 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 by A4, A12, A19, XXREAL_0: 1;

 suppose that

 A20: n = 1 and

 A21: ( len G) = 2;

 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 thesis by A20, A22, FINSEQ_1: 40;

 end;

 suppose that

 A23: n = 1 and

 A24: (1 + 1) < ( len G);

 (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 thesis by A8, A10, A23, A27;

 end;

 suppose that

 A28: 1 < n and

 A29: ( len G) = (n + 1);

 (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 thesis by A8, A10, A33;

 end;

 suppose that

 A34: 1 < n and

 A35: (n + 1) < ( len G);



 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 thesis by A8, A10, A38;

 end;

 end;

 end;