:: Properties of Connected Subsets of the Real Line :: by Artur Korni{\l}owicz :: :: Received February 22, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, SUBSET_1, MEMBERED, PRE_TOPC, METRIC_1, STRUCT_0, XXREAL_2, RCOMP_1, TARSKI, ORDINAL2, SEQ_4, TOPMETR, XREAL_0, ORDINAL1, XXREAL_1, RELAT_2, CARD_1, ARYTM_3, XXREAL_0, REAL_1, ARYTM_1, LIMFUNC1, ZFMISC_1, TOPS_1, RELAT_1, SETFAM_1, FINSET_1, ORDERS_1, WELLORD1, FINSEQ_1, PARTFUN1, WELLORD2, FUNCT_1, NAT_1, RCOMP_3, MEASURE5; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, WELLORD1, ORDERS_1, WELLORD2, RELAT_2, CARD_1, MEMBERED, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, NAT_D, LIMFUNC1, XXREAL_1, XXREAL_2, SEQM_3, FINSEQ_1, SEQ_4, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, TOPS_2, COMPTS_1, CONNSP_1, TOPMETR, MEASURE6, TOPALG_2, TOPREALB; constructors WELLORD1, WELLORD2, ORDERS_1, PROB_1, LIMFUNC1, BINARITH, TOPS_1, CONNSP_1, COMPTS_1, MEASURE6, TOPREALB, SEQ_1, BORSUK_6, NAT_D, SEQ_4; registrations XBOOLE_0, SUBSET_1, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, RCOMP_1, FCONT_3, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, TOPMETR, MEASURE6, BORSUK_2, SPRECT_1, TOPREAL6, TOPALG_2, TOPREALB, FINSET_1, VALUED_0, XXREAL_2, CARD_1, XXREAL_1, SEQ_4, WELLORD2; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions FUNCT_1, TOPS_2, RELAT_2, ORDERS_1, TARSKI, XBOOLE_0, SEQM_3, CONNSP_1, TOPALG_2, SUBSET_1, WELLORD1, STRUCT_0, LIMFUNC1, PROB_1, SETFAM_1, TOPMETR, XXREAL_2; theorems PRE_TOPC, XREAL_0, FUNCT_2, INT_1, TOPS_2, FUNCT_1, TOPMETR, RELAT_1, TARSKI, ZFMISC_1, JORDAN5A, FINSEQ_1, XBOOLE_1, COMPTS_1, SETFAM_1, XBOOLE_0, FINSEQ_3, NAT_1, RCOMP_1, SEQM_3, FINSEQ_5, HEINE, TOPS_1, CONNSP_1, TOPREALA, TOPREALB, ORDINAL1, ORDERS_1, RELAT_2, CARD_2, MEMBERED, SEQ_4, FINSEQ_4, TOPREAL6, TREAL_1, BORSUK_5, TOPS_3, TEX_1, XREAL_1, WELLORD2, XXREAL_0, XXREAL_1, PARTFUN1, XXREAL_2, MEASURE6; schemes NAT_1, RELSET_1, FINSET_1, FRAENKEL, FINSEQ_1, RECDEF_1; begin :: Preliminaries 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 Th1: for X being non empty bounded_below real-membered set, Y being 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 Th2: for X being non empty bounded_above real-membered set, Y being 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 Th3: for X, Y being 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 :: Intervals reserve a, b, r, s for real number; registration let r be real number, s be ext-real number; cluster [.r,s.[ -> bounded_below; coherence proof take r; let x be ext-real number; thus thesis by XXREAL_1:3; end; cluster ].s,r.] -> bounded_above; coherence proof take r; let x be ext-real number; 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 ext-real number; 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 ext-real number; 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 ext-real number; thus thesis by XXREAL_1:4; end; ].r,s.[ is bounded_below proof take r; let x be ext-real number; 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 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 < b ex a st a in X & a < r+b proof let b such that A6: 0 < b and A7: for a st a in X holds a >= 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 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 ex a st a in X & s-b < a proof let b such that A6: 0 < b and A7: for a st a in X holds a <= s-b; per cases; suppose s - b <= r; then A8: (r+s)/2 > 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 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 < b ex a st a in X & a < r+b proof let b such that A6: 0 < b and A7: for a st a in X holds a >= 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 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 ex a st a in X & s-b < a proof let b such that A6: 0 < b and A7: for a st a in X holds a <= s-b; per cases; suppose s - b <= r; then A8: (r+s)/2 > 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 :: Halflines theorem 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 set; 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,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 set; 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) by XXREAL_2:def 9; 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) by XXREAL_2:def 10; 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); left_open_halfline a is not 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 ext-real number; 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 set; 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 ext-real number; thus thesis by XXREAL_1:233; end; let r, s be ext-real number; 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 set; 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; right_open_halfline a is not bounded_above by Lm2; hence A is non bounded_above by XXREAL_1:22,XXREAL_2:43; let r, s be ext-real number; 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 set; 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 ext-real number; thus thesis by XXREAL_1:235; end; thus A is non bounded_above by Lm2; let r, s be ext-real number; 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 set; 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 Th9: upper_bound left_closed_halfline(a) = a proof set X = left_closed_halfline(a); A1: for s st 0 < s 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 Th10: upper_bound left_open_halfline(a) = a proof set X = left_open_halfline(a); A1: for s st 0 < s 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 Th11: lower_bound right_closed_halfline(a) = a proof set X = right_closed_halfline(a); A1: for s st 0 < s 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 Th12: lower_bound right_open_halfline(a) = a proof set X = right_open_halfline(a); A1: for s st 0 < s 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 :: Connectedness registration cluster [#]REAL -> interval non bounded_below non bounded_above; coherence; end; theorem Th13: for X being 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 Th14: for X being 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 set; 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 Th15: for X being 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 set; 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 Th16: for X being 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 set; 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 Th17: for X being 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 set; 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 Th18: for X being 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 set; 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 Th19: for X being 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 set; 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 Th20: for X being 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 set; 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 Th21: for X being interval Subset of REAL st X is not 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: X is not 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 set; assume A4: x in left_closed_halfline(upper_bound X); then reconsider x as Real; x is not LowerBound of X by A1,XXREAL_2:def 9; then consider r being ext-real number such that A5: r in X and A6: x > r by XXREAL_2:def 2; reconsider r as real number 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 Th22: for X being 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 set; 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 Th23: for X being non empty interval Subset of REAL st X is not 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: X is not 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 set; assume A4: x in left_open_halfline(upper_bound X); then reconsider x as Real; x is not LowerBound of X by A1,XXREAL_2:def 9; then consider r being ext-real number such that A5: r in X & x > r by XXREAL_2:def 2; reconsider r as real number 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 Th24: for X being 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 set; 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 Th25: for X being interval Subset of REAL st X is bounded_below & X is not 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: X is not bounded_above and A3: lower_bound X in X; thus X c= right_closed_halfline(lower_bound X) by A1,Th24; let x be set; assume A4: x in right_closed_halfline(lower_bound X); then reconsider x as Real; x is not UpperBound of X by A2,XXREAL_2:def 10; then consider r being ext-real number such that A5: r in X and A6: x < r by XXREAL_2:def 1; reconsider r as real number 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 Th26: for X being 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 set; 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 Th27: for X being non empty interval Subset of REAL st X is bounded_below & X is not 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: X is not 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 set; assume A4: x in right_open_halfline(lower_bound X); then reconsider x as Real; x is not UpperBound of X by A2,XXREAL_2:def 10; then consider r being ext-real number 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 number by A5; [.s,r.] c= X & x in [.s,r.] by A5,A6,XXREAL_1:1,XXREAL_2:def 12; hence thesis; end; theorem Th28: for X being interval Subset of REAL st X is not bounded_above & X is not bounded_below holds X = REAL proof let X be interval Subset of REAL; assume that A1: X is not bounded_above and A2: X is not bounded_below; thus X c= REAL; let x be set; assume x in REAL; then reconsider x as Real; x is not UpperBound of X by A1,XXREAL_2:def 10; then consider r being ext-real number such that A3: r in X & r > x by XXREAL_2:def 1; reconsider r as real number by A3; x is not LowerBound of X by A2,XXREAL_2:def 9; then consider s being ext-real number such that A4: s in X & s < x by XXREAL_2:def 2; reconsider s as real number by A4; [.s,r.] c= X & x in [.s,r.] by A3,A4,XXREAL_1:1,XXREAL_2:def 12; hence thesis; end; theorem Th29: for X being 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 being set 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 being set st p in X & q in X & p <> q by ZFMISC_1:def 10; 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: X is not real-bounded; per cases by A3; suppose A4: X is not 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: X is not 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 X is not bounded_above & X is not bounded_below; hence thesis by Th28; end; end; end; theorem Th30: for X being 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 Th31: for X, Y being 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 set; 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 being real number 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,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 being real number 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 being real number 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,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 being real number 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 being real number 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,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 being real number 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,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 being real number 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 being real number 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 being real number 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,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,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 being real number 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,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 being real number 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,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 being real number 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 :: R^1 theorem Th32: for X being 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 for X being 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 Th34: for X being 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 Th35: for X being 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 for X being 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 set; 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 for X being 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 Th38: for X being 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 set; 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 Th39: for X being 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 set; 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 proof thus [#](T|X) is interval by PRE_TOPC:def 5; end; 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 proof let X be Subset of R^1; assume A1: X is connected; let a be ext-real number; thus thesis by A1,BORSUK_5:77; end; cluster interval -> connected for Subset of R^1; coherence proof let X be Subset of R^1 such that A2: X is interval; A3: X is Subset of REAL by MEMBERED:3; per cases by A2,A3,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 A4: X = left_closed_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 = left_open_halfline(a); then consider a such that A5: X = left_open_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_closed_halfline(a); then consider a such that A6: X = right_closed_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 st X = right_open_halfline(a); then consider a such that A7: X = right_open_halfline(a); reconsider A=X as non empty interval Subset of R^1 by A7; 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 :: Closed Interval TSpace 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 r <= s implies for A being 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,44; hence thesis by A1,XBOOLE_1:1; end; theorem Th41: r <= s implies for X being 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 set; assume A8: x in C1; then reconsider x as Real by A1; 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 set; assume A11: x in A; then reconsider x as Real by A3; 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 Th42: r <= s implies for X being 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 set; assume A8: x in C1; then reconsider x as Real by A1; 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 set; assume A11: x in A; then reconsider x as Real by A3; 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 Th43: for X being Subset of Closed-Interval-TSpace(r,s), Y being 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 Th44: r <= s implies for X being open connected Subset of Closed-Interval-TSpace(r,s) holds X is empty or X = [.r,s.] or (ex a being real number st r < a & a <= s & X = [.r,a.[) or (ex a being real number st r <= a & a < s & X = ].a,s.]) or ex a, b being real number 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 ,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 < b and A13: Y = [.a,b.[; A14: b <= s by A2,A12,A13,XXREAL_1:52; A15: r <= a by A2,A12,A13,XXREAL_1:52; now assume r <> 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 < b and A19: Y = ].a,b.]; A20: r <= a by A2,A18,A19,XXREAL_1:53; A21: b <= s by A2,A18,A19,XXREAL_1:53; now assume b <> 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 :: Minimal cover of an interval deffunc F(set) = $1; defpred P[set,set] means $1 c= $2; theorem Th45: for T being 1-sorted, F being finite Subset-Family of T for F1 being Subset-Family of T st F is Cover of T & F1 = F \ {X where X is Subset of T: X in F & ex Y being 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 is Subset of T: X in F & ex Y being Subset of T st Y in F & X c< Y}; set ZAW = {X where X is Subset of T: X in F & ex Y being Subset of T st Y in F & X c< Y}; thus the carrier of T c= union F1 proof let t be set; assume t in the carrier of T; then consider Z being set such that A3: t in Z and A4: Z in F by A1,TARSKI:def 4; set ALL = {X where X is Subset of T: Z c< X & X in F}; per cases; suppose A5: ALL is empty; now assume Z in ZAW; then consider X being Subset of T such that A6: Z = X and X in F and A7: ex Y being Subset of T st Y in F & X c< Y; consider Y being 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 being set such that A9: w in ALL by XBOOLE_0:def 1; consider R being Relation of ALL such that A10: for x, y being set holds [x,y] in R iff x in ALL & y in ALL & P [x,y] from RELSET_1:sch 1; A11: R is_reflexive_in ALL proof let x be set; thus thesis by A10; end; 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 set; assume that A14: x in ALL and y in ALL and A15: z in ALL; assume [x,y] in R & [y,z] in R; then x c= y & y c= z by A10; then x c= z by XBOOLE_1:1; hence thesis by A10,A14,A15; end; let x, y be set; assume that x in ALL and y in ALL; assume [x,y] in R & [y,x] in R; hence x c= y & y c= x by A10; end; A16: R is reflexive by A11,A12,RELAT_2:def 9; ALL has_upper_Zorn_property_wrt R proof let Y be set such that A17: Y c= ALL and A18: R |_2 Y is being_linear-order; per cases; suppose A19: Y is non empty; defpred U[set] means $1 is non empty & $1 c= Y implies union $1 in Y; take union Y; A20: U[{}]; A21: for A, B being set st A in Y & B in Y holds A \/ B in Y proof A22: R |_2 Y c= R by XBOOLE_1:17; R |_2 Y is connected by A18,ORDERS_1:def 5; then A23: R |_2 Y is_connected_in field (R |_2 Y) by RELAT_2:def 14; let A, B be set such that A24: A in Y & B in Y; field(R |_2 Y) = Y by A12,A16,A17,ORDERS_1:71; then [A,B] in R |_2 Y or [B,A] in R |_2 Y or A = B by A24,A23, RELAT_2:def 6; then A c= B or B c= A by A10,A22; hence thesis by A24,XBOOLE_1:12; end; A25: for x, B being set st x in Y & B c= Y & U[B] holds U[B \/ {x}] proof let x, B be set such that A26: x in Y and A27: B c= Y & U[B] and B \/ {x} is non empty and B \/ {x} c= Y; A28: union {x} = x by ZFMISC_1:25; per cases; suppose B is empty; hence thesis by A26,ZFMISC_1:25; end; suppose B is non empty; then x \/ union B in Y by A21,A26,A27; hence thesis by A28,ZFMISC_1:78; end; end; consider y being set such that A29: y in Y by A19,XBOOLE_0:def 1; y in ALL by A17,A29; then consider X being Subset of T such that A30: X = y and A31: Z c< X and X in F; A32: X c= union Y by A29,A30,ZFMISC_1:74; then A33: Z <> union Y by A31,XBOOLE_0:def 8; Z c= X by A31,XBOOLE_0:def 8; then Z c= union Y by A32,XBOOLE_1:1; then A34: Z c< union Y by A33,XBOOLE_0:def 8; A35: ALL c= F proof let x be set; assume x in ALL; then ex X being Subset of T st X = x & Z c< X & X in F; hence thesis; end; then A36: Y c= F by A17,XBOOLE_1:1; A37: Y is finite by A17,A35; U[Y] from FINSET_1:sch 2(A37,A20,A25); then union Y in F by A19,A36; hence A38: union Y in ALL by A34; let z be set; assume A39: z in Y; then P[z,union Y] by ZFMISC_1:74; hence thesis by A10,A17,A38,A39; end; suppose A40: Y is empty; take w; thus w in ALL by A9; thus thesis by A40; end; end; then consider M being set such that A41: M is_maximal_in R by A12,A13,ORDERS_1:63; A42: M in field R by A41,ORDERS_1:def 11; then A43: ex X being Subset of T st X = M & Z c< X & X in F by A12; now assume M in ZAW; then consider H being Subset of T such that A44: M = H and H in F and A45: ex Y being Subset of T st Y in F & H c< Y; consider Y being Subset of T such that A46: Y in F and A47: H c< Y by A45; Z c< Y by A43,A44,A47,XBOOLE_1:56; then A48: Y in ALL by A46; H c= Y by A47,XBOOLE_0:def 8; then [M,Y] in R by A10,A12,A42,A44,A48; hence contradiction by A12,A41,A44,A47,A48,ORDERS_1:def 11; end; then A49: M in F1 by A2,A43,XBOOLE_0:def 5; Z c= M by A43,XBOOLE_0:def 8; hence thesis by A3,A49,TARSKI:def 4; end; end; end; theorem Th46: for S being 1-element 1-sorted, s being Point of S, F being 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 being 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 being 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 being set st x in Z holds x in {s} by A4,A2,A5; let x be set; thus thesis by A3,TARSKI:def 1; end; hence thesis by A4; end; definition let T be TopStruct, F be Subset-Family of T; attr F is connected means :Def1: for X being 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 set; 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 being Subset of T holds P in F implies P is open by TARSKI:def 1 ; thus for P being Subset of T holds P in F implies P is closed by TARSKI:def 1; thus for P being 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 being 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 proof let a be set; assume a in rng f; hence thesis by A1,A3,TARSKI:def 1; end; 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 Th47: for L being TopSpace, G, G1 being Subset-Family of L st G is Cover of L & G is finite for ALL being set st G1 = G \ {X where X is Subset of L: X in G & ex Y being Subset of L st Y in G & X c< Y} & ALL = {C where C is 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 is Subset of L: X in G & ex Y being Subset of L st Y in G & X c< Y}; assume that A3: G1 = G \ ZAW and A4: ALL = {C where C is 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 is Subset-Family of L: D in bool G1}; take x = meet Y; A10: ALL c= E proof let a be set; assume a in ALL; then ex C being 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 being 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,ORDERS_1:def 5; then A17: R |_2 Y is_connected_in field (R |_2 Y) by RELAT_2:def 14; 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,RELAT_2:def 6; 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 being set such that A19: y in Y by A9,XBOOLE_0:def 1; y in ALL by A7,A19; then A20: ex C being 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 set; assume A24: a in the carrier of L; meet Y in ALL by A7,A9,A22; then consider C being 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 Th48: for L being TopSpace, G, ALL being set st ALL = {C where C is Subset-Family of L: C is Cover of L & C c= G} for M being set st M is_minimal_in RelIncl ALL & M in field RelIncl ALL for A1 being Subset of L st A1 in M holds not ex A2, A3 being 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 is 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 being 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 being 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 set; 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 being 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,XBOOLE_1:1; 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,ORDERS_1:def 12; end; definition let r, s be real number; let F be Subset-Family of Closed-Interval-TSpace(r,s) such that B1: F is Cover of Closed-Interval-TSpace(r,s) and B2: F is open and B3: F is connected and B4: r <= s; mode IntervalCover of F -> FinSequence of bool REAL means :Def2: rng it c= F & union rng it = [.r,s.] & (for n being 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 being real number st r < p & p <= s & it.1 = [.r,p.[) & (ex p being real number st r <= p & p < s & it.len it = ].p,s.]) & for n being Nat st 1 < n & n < len it ex p, q being real number st r <= p & p < q & q <= s & it.n = ].p,q.[ ); existence proof per cases; suppose A1: [.r,s.] in F; take f = <*[.r,s.]*>; A2: rng f = {[.r,s.]} by FINSEQ_1:38; thus rng f c= F proof let a be set; assume a in rng f; hence thesis by A1,A2,TARSKI:def 1; end; thus union rng f = [.r,s.] by A2,ZFMISC_1:25; thus thesis by B4,A1,Lm3; end; suppose A3: not [.r,s.] in F; set L = Closed-Interval-TSpace(r,s); A4: the carrier of L = [.r,s.] by B4,TOPMETR:18; A5: now let A be Subset of L; thus A is bounded_above bounded_below by A4,XXREAL_2:43,44; hence A is real-bounded Subset of REAL by A4,XBOOLE_1:1; end; L is compact by B4,HEINE:4; then [#]L is compact by COMPTS_1:1; then consider G being Subset-Family of L such that A6: G c= F and A7: G is Cover of [#]L and A8: G is finite by B1,B2,COMPTS_1:def 4; set ZAW = {X where X is Subset of L: X in G & ex Y being Subset of L st Y in G & X c< Y}; set G1 = G \ ZAW; set ALL = {C where C is Subset-Family of L: C is Cover of L & C c= G1}; set R = RelIncl ALL; A9: R is_antisymmetric_in ALL by WELLORD2:21; set RM = {lower_bound ].c,s.] where c is Real: ].c,s.] in G1}; set LM = {upper_bound [.r,b.[ where b is Real: [.r,b.[ in G1}; A10: G1 c= G by XBOOLE_1:36; then A11: G1 c= F by A6,XBOOLE_1:1; A12: for X being 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 B3,A11,Def1; reconsider Y = X as Subset of REAL by A4,XBOOLE_1:1; Y is interval by Th43; hence thesis; end; reconsider T = L as non empty connected TopSpace by B4,TREAL_1:20; set LM1 = {upper_bound E where E is Subset of L: E in G1}; A13: LM c= LM1 proof let x be set; assume x in LM; then ex b being Real st x = upper_bound [.r,b.[ & [.r,b.[ in G1; hence thesis; end; A14: LM c= REAL proof let x be set; assume x in LM; then ex b being Real st x = upper_bound [.r,b.[ & [.r,b.[ in G1; hence thesis; end; set RM1 = {lower_bound E where E is Subset of L: E in G1}; A15: RM c= RM1 proof let x be set; assume x in RM; then ex b being Real st x = lower_bound ].b,s.] & ].b,s.] in G1; hence thesis; end; A16: RM c= REAL proof let x be set; assume x in RM; then ex b being Real st x = lower_bound ].b,s.] & ].b,s.] in G1; hence thesis; end; A17: field R = ALL by WELLORD2:def 1; R is_reflexive_in ALL & R is_transitive_in ALL by WELLORD2:19,20; then R partially_orders ALL by A9,ORDERS_1:def 7; then consider M being set such that A18: M is_minimal_in R by A7,A8,A17,Th47,ORDERS_1:64; A19: M in field R by A18,ORDERS_1:def 12; then consider C being Subset-Family of L such that A20: M = C and A21: C is Cover of L and A22: C c= G1 by A17; A23: union C = [#]L by A21,SETFAM_1:45; A24: s in [.r,s.] by B4,XXREAL_1:1; then consider R2 being set such that A25: s in R2 and A26: R2 in C by A4,A23,TARSKI:def 4; r in [.r,s.] by B4,XXREAL_1:1; then consider R1 being set such that A27: r in R1 and A28: R1 in C by A4,A23,TARSKI:def 4; A29: R1 in G1 by A22,A28; then A30: R1 in F by A11; A31: R2 in G1 by A22,A26; then A32: R2 in F by A11; reconsider R1, R2 as open connected Subset of L by B2,B3,A11,A29,A31,Def1 ,TOPS_2:def 1; A33: now per cases by B4,A3,A25,A32,Th44; suppose ex a being real number st r < a & a <= s & R2 = [.r,a.[; hence RM is non empty by A25,XXREAL_1:3; end; suppose ex a being real number st r <= a & a < s & R2 = ].a,s.]; then consider a being real number such that r <= a and a < s and A34: R2 = ].a,s.]; a is Real by XREAL_0:def 1; then lower_bound ].a,s.] in RM by A22,A26,A34; hence RM is non empty; end; suppose ex a, b being real number st r <= a & a < b & b <= s & R2 = ].a,b.[; hence RM is non empty by A25,XXREAL_1:4; end; end; A35: now per cases by B4,A3,A27,A30,Th44; suppose ex a being real number st r < a & a <= s & R1 = [.r,a.[; then consider a being real number such that r < a and a <= s and A36: R1 = [.r,a.[; a is Real by XREAL_0:def 1; then upper_bound [.r,a.[ in LM by A22,A28,A36; hence LM is non empty; end; suppose ex a being real number st r <= a & a < s & R1 = ].a,s.]; hence LM is non empty by A27,XXREAL_1:2; end; suppose ex a, b being real number st r <= a & a < b & b <= s & R1 = ].a,b.[; hence LM is non empty by A27,XXREAL_1:4; end; end; A37: G1 is finite by A8; RM1 is finite from FRAENKEL:sch 21(A37); then reconsider RM as non empty finite Subset of REAL by A15,A33,A16; F c= bool REAL proof let a be set; assume a in F; then a c= REAL by A4,XBOOLE_1:1; hence thesis; end; then G1 c= bool REAL by A11,XBOOLE_1:1; then reconsider X = C as non empty finite Subset-Family of REAL by A8 ,A22,A28,XBOOLE_1:1; LM1 is finite from FRAENKEL:sch 21(A37); then reconsider LM as non empty finite Subset of REAL by A13,A35,A14; reconsider kL = max LM as Real by XREAL_0:def 1; set LEWY = [.r,kL.[; kL in LM by XXREAL_2:def 8; then consider b being Real such that A38: kL = upper_bound [.r,b.[ and A39: [.r,b.[ in G1; A40: union G = [#]L by A7,SETFAM_1:45; A41: now consider x being set such that A42: x in the carrier of L by XBOOLE_0:def 1; consider g being set such that A43: x in g and A44: g in G by A40,A42,TARSKI:def 4; {} c= g by XBOOLE_1:2; then A45: {} c< g by A43,XBOOLE_0:def 8; assume A46: {} in G1; then {} in G by XBOOLE_0:def 5; then {} in ZAW by A44,A45; hence contradiction by A46,XBOOLE_0:def 5; end; then A47: upper_bound LEWY = kL by A38,A39,Th5,XXREAL_1:27; A48: r < b by A41,A39,XXREAL_1:27; then r < kL by A38,Th5; then A49: lower_bound LEWY = r by Th4; reconsider LEWY as non empty Subset of L by A41,A38,A39,Th5,XXREAL_1:27; A50: kL = b by A41,A38,A39,Th5,XXREAL_1:27; A51: for A being Subset of L st r in A & A in G1 holds A = LEWY proof let A be Subset of L; assume that A52: r in A and A53: A in G1; A54: A in F & A is open by B2,A11,A53,TOPS_2:def 1; A55: now assume A56: (ex a being real number st r <= a & a < s & A = ].a,s.]) or ex a, b being real number st r <= a & a < b & b <= s & A = ].a,b.[; per cases by A56; suppose ex a being real number st r <= a & a < s & A = ].a,s.]; hence contradiction by A52,XXREAL_1:2; end; suppose ex a, b being real number st r <= a & a < b & b <= s & A = ].a,b.[; hence contradiction by A52,XXREAL_1:4; end; end; A is connected by B3,A11,A53,Def1; then consider ak being real number such that A57: r < ak and ak <= s and A58: A = [.r,ak.[ by B4,A3,A52,A54,A55,Th44; A59: ak is Real by XREAL_0:def 1; A60: A c= LEWY proof upper_bound A = ak by A57,A58,Th5; then ak in LM by A53,A58,A59; then A61: ak <= kL by XXREAL_2:def 8; let a be set; assume A62: a in A; then a in [.r,s.] by A4; then reconsider a as Real; a < ak by A58,A62,XXREAL_1:3; then A63: a < kL by A61,XXREAL_0:2; r <= a by A58,A62,XXREAL_1:3; hence thesis by A63,XXREAL_1:3; end; assume A <> LEWY; then A c< LEWY by A60,XBOOLE_0:def 8; then A in ZAW by A10,A39,A50,A53; hence contradiction by A53,XBOOLE_0:def 5; end; then reconsider LLEWY = LEWY as Element of X by A22,A27,A28; reconsider pP = min RM as Real by XREAL_0:def 1; set PRAWY = ].pP,s.]; pP in RM by XXREAL_2:def 7; then consider b being Real such that A64: pP = lower_bound ].b,s.] and A65: ].b,s.] in G1; A66: lower_bound PRAWY = pP by A41,A64,A65,Th6,XXREAL_1:26; A67: b < s by A41,A65,XXREAL_1:26; then pP < s by A64,Th6; then A68: upper_bound PRAWY = s by Th7; reconsider PRAWY as non empty Subset of L by A41,A64,A65,Th6,XXREAL_1:26; A69: pP = b by A41,A64,A65,Th6,XXREAL_1:26; A70: for A being Subset of L st A in G1 & A <> LEWY & A <> PRAWY ex a, b being Real st a < b & A = ].a,b.[ proof let A be Subset of L such that A71: A in G1 and A72: A <> LEWY and A73: A <> PRAWY; A74: A in F & A is open connected by B3,B2,A11,A71,Def1,TOPS_2:def 1; per cases by B4,A3,A41,A71,A74,Th44; suppose ex a being real number st r < a & a <= s & A = [.r,a.[; then consider a being real number such that r < a and a <= s and A75: A = [.r,a.[; per cases; suppose a <= kL; then A c= LEWY by A75,XXREAL_1:38; then A c< LEWY by A72,XBOOLE_0:def 8; then A in ZAW by A10,A39,A50,A71; hence thesis by A71,XBOOLE_0:def 5; end; suppose a > kL; then LEWY c= A by A75,XXREAL_1:38; then LEWY c< A by A72,XBOOLE_0:def 8; then LEWY in ZAW by A10,A39,A50,A71; hence thesis by A39,A50,XBOOLE_0:def 5; end; end; suppose ex a being real number st r <= a & a < s & A = ].a,s.]; then consider a being real number such that r <= a and a < s and A76: A = ].a,s.]; per cases; suppose a >= pP; then A c= PRAWY by A76,XXREAL_1:42; then A c< PRAWY by A73,XBOOLE_0:def 8; then A in ZAW by A10,A65,A69,A71; hence thesis by A71,XBOOLE_0:def 5; end; suppose a < pP; then PRAWY c= A by A76,XXREAL_1:42; then PRAWY c< A by A73,XBOOLE_0:def 8; then PRAWY in ZAW by A10,A65,A69,A71; hence thesis by A65,A69,XBOOLE_0:def 5; end; end; suppose ex a, b being real number st r <= a & a < b & b <= s & A = ].a,b.[; then consider a, b being real number such that r <= a and A77: a < b and b <= s and A78: A = ].a,b.[; reconsider a, b as Real by XREAL_0:def 1; take a, b; thus thesis by A77,A78; end; end; A79: for A being Subset of L st A in G1 & upper_bound A in A holds A = PRAWY proof let A be Subset of L such that A80: A in G1 and A81: upper_bound A in A and A82: A <> PRAWY; A <> LEWY by A47,A81,XXREAL_1:3; then consider a, b being Real such that A83: a < b and A84: A = ].a,b.[ by A70,A80,A82; upper_bound A = b by A83,A84,TOPREAL6:17; hence contradiction by A81,A84,XXREAL_1:4; end; defpred F[set,set,set] means ex S being Element of X st S = $2 & upper_bound S in $3; A85: X c= F by A11,A22,XBOOLE_1:1; A86: for Z being 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 A87: Z in X; then Z is non empty interval by A41,A12,A22; hence thesis by B2,A85,A87,Th43,TOPS_2:def 1; end; A88: for n being Element of NAT st 1 <= n & n < card X for x being Element of X ex y being Element of X st F[n,x,y] proof let n be Element of NAT such that 1 <= n and n < card X; let x be Element of X; reconsider x1 = x as Subset of REAL; A89: x1 is non empty by A86; A90: x c= union X by ZFMISC_1:74; then x c= [.r,s.] by A4,A23; then x1 is bounded_above by XXREAL_2:43; then upper_bound x is Element of L by A4,A23,A89,A90,Th2; then consider y being set such that A91: upper_bound x in y and A92: y in X by A23,TARSKI:def 4; reconsider y as Element of X by A92; take y, x; thus thesis by A91; end; consider IT being FinSequence of X such that A93: len IT = card X and A94: IT.1 = LLEWY or card X = 0 and A95: for n being Element of NAT st 1 <= n & n < card X holds F[n,IT .n,IT.(n+1)] from RECDEF_1:sch 4(A88); A96: 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; A97: IT is non empty by A93; then A98: rng IT is non empty; then A99: 1 in dom IT by FINSEQ_3:32; then A100: IT/.1 = IT.1 by PARTFUN1:def 6; A101: for n being 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 A96; end; A102: for n being Nat st n in dom IT holds IT.n in G1 & IT/.n in G1 proof let n be Nat; assume n in dom IT; then IT.n = IT/.n & IT.n in X by A101,PARTFUN1:def 6; hence thesis by A22; end; A103: for i being Nat st i in dom IT for x being Point of L st x < upper_bound(IT/.i) ex j being Nat st j in dom IT & j <= i & x in IT/.j proof defpred Q[Nat] means $1 in dom IT implies for x being Point of L st x < upper_bound(IT/.$1) ex j being Nat st j in dom IT & j <= $1 & x in IT/.j; A104: Q[n] implies Q[n+1] proof assume that A105: Q[n] and A106: n+1 in dom IT; A107: IT/.(n+1) = IT.(n+1) by A106,PARTFUN1:def 6; let x be Point of L such that A108: x < upper_bound(IT/.(n+1)); per cases by A106,TOPREALA:2; suppose A109: n = 0; take 1; thus 1 in dom IT by A98,FINSEQ_3:32; thus 1 <= n+1 by A109; r <= x by A4,XXREAL_1:1; hence thesis by A47,A94,A108,A107,A109,XXREAL_1:3; end; suppose A110: n in dom IT; n+1 <= len IT by A106,FINSEQ_3:25; then A111: n < len IT by NAT_1:13; 1 <= n by A110,FINSEQ_3:25; then A112: ex S being Element of X st S = IT.n & upper_bound S in IT. ( n+1) by A93,A95,A110,A111; IT/.(n+1) in X by A101,A106; then A113: IT/.(n+1) is bounded_below by A5; IT/.n = IT.n by A110,PARTFUN1:def 6; then A114: lower_bound(IT/.(n+1)) <= upper_bound(IT/.n) by A107,A113,A112, SEQ_4:def 2; A115: IT/.(n+1) is interval Subset of REAL & IT/.(n+1) is non empty by A41,A12,A102,A106; per cases by XXREAL_0:1; suppose x < upper_bound(IT/.n); then consider j being Nat such that A116: j in dom IT and A117: j <= n and A118: x in IT/.j by A105,A110; take j; thus j in dom IT by A116; j+0 < n+1 by A117,XREAL_1:8; hence j <= n+1; thus thesis by A118; end; suppose A119: x = upper_bound(IT/.n); take n+1; thus n+1 in dom IT by A106; thus n+1 <= n+1; thus thesis by A107,A110,A112,A119,PARTFUN1:def 6; end; suppose A120: x > upper_bound(IT/.n); take n+1; thus n+1 in dom IT by A106; thus n+1 <= n+1; lower_bound(IT/.(n+1)) < x by A114,A120,XXREAL_0:2; hence thesis by A108,A115,Th30; end; end; end; A121: Q[0] by FINSEQ_3:24; A122: Q[n] from NAT_1:sch 2(A121,A104); let i be Nat; assume i in dom IT; hence thesis by A122; end; A123: s in ].b,s.] by A67,XXREAL_1:2; A124: for i being Nat st i in dom IT for j being Nat st j in dom IT & i < j ex y being Point of L st y in IT/.j & for x being Point of L st x in IT/.i holds x < y proof let i be Nat such that A125: i in dom IT; defpred W[Nat] means $1 in dom IT & i < $1 implies ex y being Point of L st y in IT/.$1 & for x being Point of L st x in IT/.i holds x < y; A126: for n holds W[n] implies W[n+1] proof let n; assume that A127: W[n] and A128: n+1 in dom IT; A129: IT/.(n+1) = IT.(n+1) by A128,PARTFUN1:def 6; assume A130: i < n+1; then A131: i <= n by NAT_1:13; per cases by A128,TOPREALA:2; suppose n = 0; then i = 0 by A130,NAT_1:13; hence thesis by A125,FINSEQ_3:24; end; suppose A132: n in dom IT; then A133: IT/.n in X by A101; then A134: IT/.n is bounded_above by A5; A135: IT/.n = IT.n by A132,PARTFUN1:def 6; then IT/.n in rng IT by A132,FUNCT_1:def 3; then A136: IT/.n is non empty & IT/.n is Subset of L by A86,A96; then upper_bound(IT/.n) in [.r,s.] by A4,A134,Th2; then A137: upper_bound(IT/.n) <= s by XXREAL_1:1; A138: IT/.(n+1) in X by A101,A128; A139: 1 <= n by A132,FINSEQ_3:25; A140: IT/.(n+1) in rng IT by A128,A129,FUNCT_1:def 3; then A141: IT/.(n+1) is open connected Subset of L by A86,A96; then A142: IT/.(n+1) is interval Subset of REAL by Th43; A143: n+1 <= len IT by A128,FINSEQ_3:25; then n is Element of NAT & n < card X by A93,NAT_1:13 ,ORDINAL1:def 12; then consider S being Element of X such that A144: S = IT.n and A145: upper_bound S in IT.(n+1) by A95,A139; IT/.(n+1) is bounded_below by A5,A141; then A146: lower_bound(IT/.(n+1)) <= upper_bound S by A129,A145,SEQ_4:def 2; A147: IT/.(n+1) is bounded_above by A5,A141; then A148: upper_bound S <= upper_bound(IT/.(n+1)) by A129,A145,SEQ_4:def 1; A149: IT/.(n+1) is non empty by A86,A96,A140; then upper_bound(IT/.(n+1)) in [.r,s.] by A4,A141,A147,Th2; then A150: upper_bound(IT/.(n+1)) <= s by XXREAL_1:1; per cases by A131,XXREAL_0:1; suppose i < n; then consider y being Point of L such that A151: y in IT/.n and A152: for x being Point of L st x in IT/.i holds x < y by A127,A132; A153: y <= upper_bound(IT/.n) by A134,A151,SEQ_4:def 1; per cases by A148,XXREAL_0:1; suppose A154: upper_bound S < upper_bound(IT/.(n+1)); set y1 = (upper_bound S + upper_bound(IT/.(n+1))) / 2; A155: upper_bound S < y1 by A154,XREAL_1:226; upper_bound S in [.r,s.] by A4,A135,A134,A136,A144,Th2; then r <= upper_bound S by XXREAL_1:1; then A156: r <= y1 by A155,XXREAL_0:2; y1 < upper_bound(IT/.(n+1)) by A154,XREAL_1:226; then y1 < s by A150,XXREAL_0:2; then reconsider y1 as Point of L by A4,A156,XXREAL_1:1; take y1; lower_bound(IT/.(n+1)) < y1 by A146,A155,XXREAL_0:2; hence y1 in IT/.(n+1) by A142,A149,A154,Th30,XREAL_1:226; let x be Point of L; assume x in IT/.i; then x < upper_bound(IT/.n) by A152,A153,XXREAL_0:2; hence thesis by A135,A144,A155,XXREAL_0:2; end; suppose A157: upper_bound S = upper_bound(IT/.(n+1)); reconsider y1 = s as Point of L by B4,A4,XXREAL_1:1; take y1; IT/.(n+1) = PRAWY by A22,A79,A129,A145,A138,A157; hence y1 in IT/.(n+1) by A67,A69,XXREAL_1:2; let x be Point of L; assume x in IT/.i; then x < upper_bound(IT/.n) by A152,A153,XXREAL_0:2; hence thesis by A137,XXREAL_0:2; end; end; suppose A158: i = n; reconsider y1 = upper_bound(IT/.n) as Element of L by A4,A134 ,A136,Th2; take y1; thus y1 in IT/.(n+1) by A129,A132,A144,A145,PARTFUN1:def 6; let x be Point of L; assume A159: x in IT/.i; A160: now set IT1 = IT|Seg n; A161: rng IT1 c= rng IT by RELAT_1:70; rng IT1 c= bool the carrier of L proof let A be set; assume A in rng IT1; then A in rng IT by A161; then A in X by A96; hence thesis; end; then reconsider FI = rng IT1 as Subset-Family of L; assume x = upper_bound(IT/.n); then A162: IT/.n = PRAWY by A22,A79,A133,A158,A159; A163: now union FI = the carrier of L proof thus union FI c= the carrier of L; let l be set; 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 being Nat such that A164: j in dom IT and A165: j <= n and A166: l in IT/.j by A103,A132; 1 <= j by A164,FINSEQ_3:25; then j in Seg n by A165,FINSEQ_1:1; then A167: IT.j in FI by A164,FUNCT_1:50; IT.j = IT/.j by A164,PARTFUN1:def 6; hence thesis by A166,A167,TARSKI:def 4; end; suppose A168: l >= upper_bound(IT/.n); n in Seg n by A139,FINSEQ_1:1; then A169: IT.n in FI by A132,FUNCT_1:50; l <= s by A4,XXREAL_1:1; then l = s by A68,A162,A168,XXREAL_0:1; hence thesis by A69,A123,A135,A162,A169,TARSKI:def 4; end; end; then A170: FI is Cover of L by SETFAM_1:def 11; assume A171: FI <> X; A172: FI c= X by A96,A161,XBOOLE_1:1; then FI c= G1 by A22,XBOOLE_1:1; then A173: FI in ALL by A170; then [FI,M] in R by A17,A19,A20,A172,WELLORD2:def 1; hence contradiction by A17,A18,A20,A171,A173,ORDERS_1:def 12; end; Seg n c= dom IT proof let x be set; A174: n+0 <= n+1 by XREAL_1:6; assume A175: x in Seg n; then reconsider x as Nat; x <= n by A175,FINSEQ_1:1; then x <= n+1 by A174,XXREAL_0:2; then A176: x <= len IT by A143,XXREAL_0:2; 1 <= x by A175,FINSEQ_1:1; hence thesis by A176,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 A93,A143,A163,XXREAL_0:2; hence contradiction by XREAL_1:6; end; x <= upper_bound(IT/.n) by A134,A158,A159,SEQ_4:def 1; hence thesis by A160,XXREAL_0:1; end; end; end; A177: W[0]; for n holds W[n] from NAT_1:sch 2(A177,A126); hence thesis; end; A178: IT is one-to-one proof let i, j be set such that A179: i in dom IT & j in dom IT and A180: IT.i = IT.j; A181: IT/.i = IT.i & IT/.j = IT.j by A179,PARTFUN1:def 6; assume A182: i <> j; reconsider i, j as Nat by A179; per cases by A182,XXREAL_0:1; suppose i < j; then ex y being Point of L st y in IT/.j & for x being Point of L st x in IT/.i holds x < y by A124,A179; hence thesis by A180,A181; end; suppose j < i; then ex y being Point of L st y in IT/.i & for x being Point of L st x in IT/.j holds x < y by A124,A179; hence thesis by A180,A181; end; end; A183: for i, j being 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 A184: i in dom IT & j in dom IT and A185: i <> j; IT/.i = IT.i & IT/.j = IT.j by A184,PARTFUN1:def 6; hence thesis by A178,A184,A185,FUNCT_1:def 4; end; A186: for A being Subset of L st s in A & A in G1 holds A = PRAWY proof let A be Subset of L; assume that A187: s in A and A188: A in G1; A189: A in F & A is open by B2,A11,A188,TOPS_2:def 1; A190: now assume A191: (ex a being real number st r < a & a <= s & A = [.r,a.[) or ex a, b being real number st r <= a & a < b & b <= s & A = ].a,b.[; per cases by A191; suppose ex a being real number st r < a & a <= s & A = [.r,a.[; hence contradiction by A187,XXREAL_1:3; end; suppose ex a, b being real number st r <= a & a < b & b <= s & A = ].a,b.[; hence contradiction by A187,XXREAL_1:4; end; end; A is connected by B3,A11,A188,Def1; then consider ak being real number such that r <= ak and A192: ak < s and A193: A = ].ak,s.] by B4,A3,A187,A189,A190,Th44; A194: ak is Real by XREAL_0:def 1; A195: A c= PRAWY proof lower_bound A = ak by A192,A193,Th6; then ak in RM by A188,A193,A194; then A196: pP <= ak by XXREAL_2:def 7; let a be set; assume A197: a in A; then a in [.r,s.] by A4; then reconsider a as Real; ak < a by A193,A197,XXREAL_1:2; then A198: pP < a by A196,XXREAL_0:2; a <= s by A193,A197,XXREAL_1:2; hence thesis by A198,XXREAL_1:2; end; assume A <> PRAWY; then A c< PRAWY by A195,XBOOLE_0:def 8; then A in ZAW by A10,A65,A69,A188; hence contradiction by A188,XBOOLE_0:def 5; end; take IT; thus rng IT c= F by A85,A96,XBOOLE_1:1; dom IT = Seg len IT by FINSEQ_1:def 3; then A199: card dom IT = card X by A93,FINSEQ_1:57; IT is Function of dom IT,X by A96,FUNCT_2:2; then A200: rng IT = X by A199,A178,FINSEQ_4:63; hence union rng IT = [.r,s.] by A4,A23; ex Z being set st s in Z & Z in C by A24,A4,A23,TARSKI:def 4; then PRAWY in X by A22,A186; then consider i being set such that A201: i in dom IT and A202: IT.i = PRAWY by A200,FUNCT_1:def 3; reconsider i as Element of NAT by A201; A203: i <= len IT by A201,FINSEQ_3:25; A204: IT/.i = IT.i by A201,PARTFUN1:def 6; A205: 1 <= i by A201,FINSEQ_3:25; A206: now assume i <> len IT; then A207: i < len IT by A203,XXREAL_0:1; then A208: ex S being Element of X st S = IT.i & upper_bound S in IT.(i+1) by A93,A95,A205; 0+1 <= i+1 & i+1 <= len IT by A207,NAT_1:13; then A209: i+1 in dom IT by FINSEQ_3:25; then IT/.(i+1) = IT.(i+1) & IT/.(i+1) in G1 by A102,PARTFUN1:def 6; then i+0 = i+1 by A68,A186,A183,A201,A202,A204,A208,A209; hence contradiction; end; A210: len IT in dom IT by A97,FINSEQ_5:6; A211: for n being Nat st 1 < n & n < len IT ex a, b being Real st r <= a & a < b & b <= s & IT/.n = ].a,b.[ proof let n be Nat such that A212: 1 < n and A213: n < len IT; A214: n in dom IT by A212,A213,FINSEQ_3:25; then IT.n in rng IT by FUNCT_1:def 3; then A215: IT/.n in rng IT by A214,PARTFUN1:def 6; then A216: IT/.n in X by A96; then A217: IT/.n in G1 & IT/.n in F by A22,A85; A218: IT/.n is open connected Subset of L by A86,A96,A215; per cases by B4,A3,A41,A217,A218,Th44; suppose ex a being real number st r < a & a <= s & IT/.n = [.r,a.[; then consider a being real number such that A219: r < a and a <= s and A220: IT/.n = [.r,a.[; r in [.r,a.[ by A219,XXREAL_1:3; hence thesis by A22,A51,A94,A99,A100,A183,A212,A214,A216,A220; end; suppose ex a being real number st r <= a & a < s & IT/.n = ].a,s.]; then consider a being real number such that r <= a and A221: a < s and A222: IT/.n = ].a,s.]; upper_bound ].a,s.] = s & s in ].a,s.] by A221,Th7,XXREAL_1:2; hence thesis by A22,A79,A210,A183,A202,A204,A206,A213,A214,A216,A222; end; suppose ex a, b being real number st r <= a & a < b & b <= s & IT /.n = ].a,b.[; then consider a, b being real number such that A223: r <= a & a < b & b <= s & IT/.n = ].a,b.[; reconsider a, b as Real by XREAL_0:def 1; take a, b; thus thesis by A223; end; end; A224: now let n be Nat such that A225: 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 A225,FINSEQ_3:25,FINSEQ_4:15; then IT/.n in rng IT by FUNCT_1:def 3; then IT/.n in X by A96; hence IT/.n is non empty by A41,A22; end; hereby assume A226: n+1 <= len IT; then A227: m < len IT by NAT_1:13; then A228: IT/.n = IT.n by A225,FINSEQ_4:15; A229: m in dom IT by A225,A227,FINSEQ_3:25; then IT/.n in rng IT by A228,FUNCT_1:def 3; then A230: IT/.n in X by A96; then A231: IT/.n in G1 by A22; A232: IT /.n is non empty real-bounded interval Subset of REAL by A5,A41,A12,A22,A230; A233: ex S being Element of X st S = IT.n & upper_bound S in IT.(n+1 ) by A93,A95,A225,A227; A234: 1 < m+1 by A225,NAT_1:13; then A235: IT/.(m+1) = IT.(m+1) by A226,FINSEQ_4:15; A236: n+1 in dom IT by A226,A234,FINSEQ_3:25; then A237: IT/.(n+1) in rng IT by A235,FUNCT_1:def 3; then A238: IT/.(n+1) in X by A96; then A239: IT/.(n+1) in G1 by A22; n+0 < n+1 by XREAL_1:6; then A240: IT/.n <> IT/.(n+1) by A183,A229,A236; A241: IT/.(n+1) is non empty real-bounded interval Subset of REAL by A5,A41,A12,A22,A238; IT/.(n+1) c= union X by A96,A237,ZFMISC_1:74; then IT/.(n+1) c= [.r,s.] by A4,A23; then A242: IT/.(n+1) is bounded_above by XXREAL_2:43; then A243: upper_bound(IT/.n) <= upper_bound(IT/.(n+1)) by A233,A228,A235, SEQ_4:def 1; hereby assume A244: 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 A22,A79,A210,A183 ,A202,A204,A206,A227,A229,A230; then IT/.n c= IT/.(n+1) by A232,A241,A243,A244,Th31; then IT/.n c< IT/.(n+1) by A240,XBOOLE_0:def 8; then IT/.n in ZAW by A10,A231,A239; hence contradiction by A22,A230,XBOOLE_0:def 5; end; thus upper_bound(IT/.n) <= upper_bound(IT/.(n+1)) by A233,A228,A235 ,A242,SEQ_4:def 1; per cases by A226,XXREAL_0:1; suppose A245: n+1 = len IT; then pP < upper_bound(IT/.n) by A202,A206,A233,A228,XXREAL_1:2; hence lower_bound(IT/.(n+1)) < upper_bound(IT/.n) by A202,A204,A206,A245 ,Th6,XXREAL_1:26; end; suppose n+1 < len IT; then consider a1, b1 being Real such that r <= a1 and A246: a1 < b1 and b1 <= s and A247: IT/.(n+1) = ].a1,b1.[ by A211,A234; a1 < upper_bound(IT/.n) by A233,A228,A235,A247,XXREAL_1:4; hence lower_bound(IT/.(n+1)) < upper_bound(IT/.n) by A246,A247, TOPREAL6:17; end; end; end; hereby let n be Nat such that A248: 1 <= n; thus A249: (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 A224 ,A248; reconsider m = n as Nat; A250: n+0 < n+1 by XREAL_1:6; then A251: 1 < m+1 by A248,XXREAL_0:2; assume A252: n+2 <= len IT; then A253: n+1+1 <= len IT; then A254: m+1 < len IT by NAT_1:13; then A255: n+1 in dom IT by A251,FINSEQ_3:25; then IT/.(n+1) = IT.(n+1) by PARTFUN1:def 6; then IT/.(n+1) in rng IT by A255,FUNCT_1:def 3; then A256: IT/.(n+1) in X by A96; 0+1 <= n+1 by XREAL_1:6; then A257: upper_bound(IT/.(n+1)) <= upper_bound(IT/.(n+1+1)) by A224,A252; assume A258: upper_bound(IT/.n) > lower_bound(IT/.(n+2)); consider a1, b1 being Real such that r <= a1 and A259: a1 < b1 and b1 <= s and A260: IT/.(n+1) = ].a1,b1.[ by A211,A251,A254; A261: lower_bound ].a1,b1.[ = a1 by A259,TOPREAL6:17; A262: upper_bound ].a1,b1.[ = b1 by A259,TOPREAL6:17; A263: IT/.(n+1) c= IT/.n \/ IT/.(n+2) proof let x be set; assume A264: x in IT/.(n+1); then reconsider x as Real; A265: a1 < x by A260,A264,XXREAL_1:4; A266: x < b1 by A260,A264,XXREAL_1:4; per cases; suppose A267: x < upper_bound(IT/.n); per cases; suppose A268: n = 1; then lower_bound(IT/.n) <= x by A4,A49,A94,A100,A256,A264, XXREAL_1:1; then x in IT/.n by A38,A50,A49,A94,A100,A267,A268,XXREAL_1:3; hence thesis by XBOOLE_0:def 3; end; suppose A269: n <> 1; n+0 < n+2 by XREAL_1:6; then A270: n < len IT by A252,XXREAL_0:2; A271: lower_bound(IT/.n) < x by A249,A253,A260,A261,A265,NAT_1:13 ,XXREAL_0:2; 1 < n by A248,A269,XXREAL_0:1; then consider a, b being Real such that r <= a and A272: a < b and b <= s and A273: IT/.n = ].a,b.[ by A211,A270; lower_bound(IT/.n) = a & upper_bound(IT/.n) = b by A272,A273, TOPREAL6:17; then x in IT/.n by A267,A273,A271,XXREAL_1:4; hence thesis by XBOOLE_0:def 3; end; end; suppose x >= upper_bound(IT/.n); then A274: x > lower_bound(IT/.(n+2)) by A258,XXREAL_0:2; per cases; suppose A275: len IT = n+2; x <= s by A4,A256,A264,XXREAL_1:1; then x in IT/.(n+2) by A66,A202,A204,A206,A274,A275,XXREAL_1:2; hence thesis by XBOOLE_0:def 3; end; suppose A276: len IT <> n+2; n+1 < n+2 by XREAL_1:6; then A277: 1 < n+2 by A251,XXREAL_0:2; n+1+1 < len IT by A252,A276,XXREAL_0:1; then consider a2, b2 being Real such that r <= a2 and A278: a2 < b2 and b2 <= s and A279: IT/.(n+2) = ].a2,b2.[ by A211,A277; upper_bound ].a2,b2.[ = b2 by A278,TOPREAL6:17; then A280: x < b2 by A257,A260,A262,A266,A279,XXREAL_0:2; lower_bound ].a2,b2.[ = a2 by A278,TOPREAL6:17; then x in IT/.(n+2) by A274,A279,A280,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 A251,XXREAL_0:2; then A281: m+2 in dom IT by A252,FINSEQ_3:25; then IT/.(n+2) = IT.(n+2) by PARTFUN1:def 6; then IT/.(n+2) in rng IT by A281,FUNCT_1:def 3; then A282: IT/.(n+2) in X by A96; m <= len IT by A250,A254,XXREAL_0:2; then A283: n in dom IT by A248,FINSEQ_3:25; then IT/.n = IT.n by PARTFUN1:def 6; then IT/.n in rng IT by A283,FUNCT_1:def 3; then A284: IT/.n in X by A96; n+1 < n+2 by XREAL_1:6; then A285: IT/.(n+2) <> IT/.(n+1) by A183,A255,A281; n+0 < n+1 by XREAL_1:6; then IT/.n <> IT/.(n+1) by A183,A283,A255; hence contradiction by A18,A19,A20,A284,A256,A282,A285,A263,Th48; end; thus [.r,s.] in F implies IT = <*[.r,s.]*> by A3; assume not [.r,s.] in F; thus ex p being real number st r < p & p <= s & IT.1 = [.r,p.[ proof take kL; thus r < kL by A38,A48,Th5; upper_bound LEWY <= upper_bound [.r,s.] by A4,SEQ_4:48; hence kL <= s by B4,A47,JORDAN5A:19; thus thesis by A94; end; thus ex p being real number st r <= p & p < s & IT.len IT = ].p,s.] proof take pP; lower_bound [.r,s.] <= lower_bound PRAWY by A4,SEQ_4:47; hence r <= pP by B4,A66,JORDAN5A:19; thus pP < s by A64,A67,Th6; thus thesis by A202,A206; end; let n be Nat such that A286: 1 < n & n < len IT; consider a, b being Real such that A287: r <= a & a < b & b <= s & IT/.n = ].a,b.[ by A211,A286; take a, b; thus thesis by A286,A287,FINSEQ_4:15; end; end; end; theorem 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 being 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 Th50: for F being Subset-Family of Closed-Interval-TSpace(r,r), C being 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 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 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 being set st a in C.1 holds a in [.r,s.] by A3,A4,TARSKI:def 4; let a be set; A5: dom C = {1} by A2,FINSEQ_1:2,def 3; assume a in [.r,s.]; then consider Z being set such that A6: a in Z and A7: Z in rng C by A3,TARSKI:def 4; ex x being set 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 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 being 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,2; end; end; A11: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A11,A4); hence thesis by A3; end; theorem 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 being 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,2; end; end; A11: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A11,A4); hence thesis by A3; end; theorem 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 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 being real number st r < p & p <= s & C.1 = [.r,p.[ by A1,A2,Def2 ; hence thesis by A3,Th4; end; end; theorem 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 being real number st r < p & p <= s & C.1 = [.r,p.[ by A1,A2,Def2 ; hence thesis by A3,XXREAL_1:3; end; end; theorem 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 being real number st r <= p & p < s & C.len C = ].p,s.] by A1,A2,Def2; hence thesis by A3,Th7; end; end; theorem 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 being real number 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 number; let F be Subset-Family of Closed-Interval-TSpace(r,s), C be IntervalCover of F such that B1: F is Cover of Closed-Interval-TSpace(r,s) & F is open & F is connected & r <= s; mode IntervalCoverPts of C -> FinSequence of REAL means :Def3: len it = len C + 1 & it.1 = r & it.len it = s & for n being 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)).[); A1: 0+1 <= len C by B1,Th51; then A2: 0+1 < A by XREAL_1:6; A3: for k being Nat st k in Seg A ex x being Element of REAL st P[k,x] proof reconsider r, s as Real by XREAL_0:def 1; let k be Nat; A4: len C + 0 < A by XREAL_1:6; assume k in Seg A; then A5: 1 <= k & k <= A by FINSEQ_1:1; per cases by A5,XXREAL_0:1; suppose A6: k = 1; take r; thus thesis by A1,A6; end; suppose A7: k = A; take s; thus thesis by A1,A4,A7; end; suppose that A8: 1 < k and A9: k < A; A10: k-1 in NAT by A8,INT_1:5; A11: k <= len C by A9,NAT_1:13; 1-1 < k-1 by A8,XREAL_1:14; then 0+1 <= k-1 by A10,NAT_1:13; then ].lower_bound(C/.(k-1+1)),upper_bound(C/.(k-1)).[ is non empty by B1 ,A10,A11,Th55; then consider x being set such that A12: x in ].lower_bound(C/.(k-1+1)),upper_bound(C/.(k-1)).[ by XBOOLE_0:def 1; reconsider x as Real by A12; take x; thus thesis by A8,A9,A12; end; end; consider p being FinSequence of REAL such that A13: dom p = Seg A and A14: for k being Nat st k in Seg A holds P[k,p.k] from FINSEQ_1:sch 5( A3); take p; thus A15: len p = len C + 1 by A13,FINSEQ_1:def 3; 1 in Seg A by A2,FINSEQ_1:1; hence p.1 = r by A14; len p in Seg A by A2,A15,FINSEQ_1:1; hence p.len p = s by A14,A15; let n be Nat; assume 1 <= n; then A16: 1+1 <= n+1 by XREAL_1:6; assume A17: n+1 < len p; 0+1 <= n+1 by XREAL_1:6; then A18: n+1 in Seg A by A15,A17,FINSEQ_1:1; n+1 <= len C by A15,A17,NAT_1:13; then p.(n+1) in ].lower_bound(C/.(n+1)),upper_bound(C/.(n+1-1)).[ by A14 ,A18,A16; hence thesis; end; end; reserve G for IntervalCoverPts of C; theorem 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 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 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 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 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 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 Element of 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 being 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,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 being Nat holds P[k] from NAT_1:sch 2(A36,A4); hence thesis by A3; end; theorem 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,Def1; 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,SEQM_3:def 1; 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,XXREAL_2:def 12; 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,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,XXREAL_2:def 12; 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,XXREAL_2:def 12; end; end; end;