:: On the Subcontinua of a Real Line
::  by Adam Grabowski
::
:: Received June 12, 2003
:: Copyright (c) 2003-2019 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, TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, ARYTM_3, TOPMETR,
      BORSUK_2, PRE_TOPC, XXREAL_0, XXREAL_1, SUBSET_1, RELAT_1, STRUCT_0,
      TREAL_1, VALUED_1, FUNCT_1, BORSUK_1, ORDINAL2, GRAPH_1, ARYTM_1,
      RELAT_2, XREAL_0, CONNSP_1, REAL_1, LIMFUNC1, METRIC_1, COMPLEX1, RAT_1,
      POWER, IRRAT_1, INT_1, XCMPLX_0, RCOMP_1, PCOMPS_1, XXREAL_2, SEQ_4,
      SETFAM_1, BORSUK_5, MEASURE5;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
      XCMPLX_0, XREAL_0, ENUMSET1, FUNCT_1, FUNCT_2, XXREAL_2, MEASURE6,
      STRUCT_0, INT_1, COMPLEX1, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, SEQ_4,
      TREAL_1, CONNSP_1, BORSUK_2, TOPMETR, LIMFUNC1, IRRAT_1, RAT_1, MEASURE5,
      METRIC_1, PCOMPS_1, XXREAL_0;
 constructors COMPLEX1, PROB_1, LIMFUNC1, POWER, CONNSP_1, TOPS_2, COMPTS_1,
      TREAL_1, MEASURE6, BORSUK_2, INTEGRA1, SEQ_4, BINOP_2, PCOMPS_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0,
      INT_1, RAT_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, TOPMETR,
      BORSUK_2, TOPREAL6, FCONT_3, RCOMP_1, MEASURE5, ORDINAL1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions XBOOLE_0, TARSKI, BORSUK_2, TOPS_2;
 equalities SUBSET_1, STRUCT_0, LIMFUNC1, PROB_1;
 expansions TARSKI, BORSUK_2, TOPS_2;
 theorems BORSUK_1, PRE_TOPC, COMPTS_1, TARSKI, TOPMETR, RCOMP_1, CONNSP_1,
      ZFMISC_1, JORDAN5A, XREAL_0, TREAL_1, XBOOLE_0, XBOOLE_1, SEQ_4,
      INTEGRA1, FUNCT_2, TOPS_1, BORSUK_4, BORSUK_2, ENUMSET1, RAT_1, METRIC_1,
      ABSVALUE, XCMPLX_1, CARD_2, INT_1, YELLOW_8, IRRAT_1, NUMBERS, XREAL_1,
      SUBSET_1, GOBOARD6, XXREAL_0, XXREAL_1, XXREAL_2, MEASURE5;

begin :: Preliminaries

::$CT

theorem
  for x1, x2, x3, x4, x5, x6 being set holds { x1, x2, x3, x4, x5, x6 }
  = { x1, x3, x6 } \/ { x2, x4, x5 }
proof
  let x1, x2, x3, x4, x5, x6 be set;
  thus { x1, x2, x3, x4, x5, x6 } c= { x1, x3, x6 } \/ { x2, x4, x5 }
  proof
    let x be object;
    assume x in { x1, x2, x3, x4, x5, x6 };
    then x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 by
ENUMSET1:def 4;
    then x in { x1, x3, x6 } or x in { x2, x4, x5 } by ENUMSET1:def 1;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in { x1, x3, x6 } \/ { x2, x4, x5 };
  then x in { x1, x3, x6 } or x in { x2, x4, x5 } by XBOOLE_0:def 3;
  then x = x1 or x = x3 or x = x6 or x = x2 or x = x4 or x = x5 by
ENUMSET1:def 1;
  hence thesis by ENUMSET1:def 4;
end;

reserve x1, x2, x3, x4, x5, x6, x7 for set;

theorem Th2:
  for x1, x2, x3, x4, x5, x6 being set st x1, x2, x3, x4, x5, x6
  are_mutually_distinct holds card {x1, x2, x3, x4, x5, x6} = 6
proof
  let x1, x2, x3, x4, x5, x6 be set;
A1: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6} by ENUMSET1:15;
  assume
A2: x1, x2, x3, x4, x5, x6 are_mutually_distinct;
  then
A3: x1 <> x3 by ZFMISC_1:def 8;
A4: x4 <> x5 by A2,ZFMISC_1:def 8;
A5: x3 <> x5 by A2,ZFMISC_1:def 8;
A6: x3 <> x4 by A2,ZFMISC_1:def 8;
A7: x2 <> x5 by A2,ZFMISC_1:def 8;
A8: x2 <> x4 by A2,ZFMISC_1:def 8;
A9: x2 <> x3 by A2,ZFMISC_1:def 8;
A10: x1 <> x5 by A2,ZFMISC_1:def 8;
A11: x1 <> x4 by A2,ZFMISC_1:def 8;
  x1 <> x2 by A2,ZFMISC_1:def 8;
  then x1, x2, x3, x4, x5 are_mutually_distinct by A3,A11,A10,A9,A8,A7,A6,A5
,A4,ZFMISC_1:def 7;
  then
A12: card {x1,x2,x3,x4,x5} = 5 by CARD_2:63;
A13: x3 <> x6 by A2,ZFMISC_1:def 8;
A14: x2 <> x6 by A2,ZFMISC_1:def 8;
A15: x5 <> x6 by A2,ZFMISC_1:def 8;
A16: x4 <> x6 by A2,ZFMISC_1:def 8;
  x1 <> x6 by A2,ZFMISC_1:def 8;
  then not x6 in {x1,x2,x3,x4,x5} by A14,A13,A16,A15,ENUMSET1:def 3;
  hence card {x1,x2,x3,x4,x5,x6} = 5+1 by A12,A1,CARD_2:41
    .= 6;
end;

theorem
  for x1, x2, x3, x4, x5, x6, x7 being set st x1, x2, x3, x4, x5, x6, x7
  are_mutually_distinct holds card {x1, x2, x3, x4, x5, x6, x7} = 7
proof
  let x1, x2, x3, x4, x5, x6, x7 be set;
A1: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7} by ENUMSET1:21;
  assume
A2: x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct;
  then
A3: x1 <> x3 by ZFMISC_1:def 9;
A4: x5 <> x7 by A2,ZFMISC_1:def 9;
A5: x4 <> x7 by A2,ZFMISC_1:def 9;
A6: x3 <> x7 by A2,ZFMISC_1:def 9;
A7: x2 <> x7 by A2,ZFMISC_1:def 9;
A8: x4 <> x6 by A2,ZFMISC_1:def 9;
A9: x4 <> x5 by A2,ZFMISC_1:def 9;
A10: x5 <> x6 by A2,ZFMISC_1:def 9;
A11: x1 <> x5 by A2,ZFMISC_1:def 9;
A12: x1 <> x4 by A2,ZFMISC_1:def 9;
A13: x3 <> x6 by A2,ZFMISC_1:def 9;
A14: x3 <> x5 by A2,ZFMISC_1:def 9;
A15: x3 <> x4 by A2,ZFMISC_1:def 9;
A16: x2 <> x6 by A2,ZFMISC_1:def 9;
A17: x2 <> x5 by A2,ZFMISC_1:def 9;
A18: x2 <> x4 by A2,ZFMISC_1:def 9;
A19: x2 <> x3 by A2,ZFMISC_1:def 9;
A20: x1 <> x6 by A2,ZFMISC_1:def 9;
  x1 <> x2 by A2,ZFMISC_1:def 9;
  then x1, x2, x3, x4, x5, x6 are_mutually_distinct by A3,A12,A11,A20,A19,A18
,A17,A16,A15,A14,A13,A9,A8,A10,ZFMISC_1:def 8;
  then
A21: card {x1,x2,x3,x4,x5,x6} = 6 by Th2;
A22: x6 <> x7 by A2,ZFMISC_1:def 9;
  x1 <> x7 by A2,ZFMISC_1:def 9;
  then not x7 in {x1,x2,x3,x4,x5,x6} by A7,A6,A5,A4,A22,ENUMSET1:def 4;
  hence card {x1,x2,x3,x4,x5,x6,x7} = 6+1 by A21,A1,CARD_2:41
    .= 7;
end;

theorem Th4:
  { x1, x2, x3 } misses { x4, x5, x6 } implies x1 <> x4 & x1 <> x5
  & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6
proof
  assume
A1: { x1, x2, x3 } misses { x4, x5, x6 };
A2: x5 in { x4, x5, x6 } by ENUMSET1:def 1;
  assume x1 = x4 or x1 = x5 or x1 = x6 or x2 = x4 or x2 = x5 or x2 = x6 or x3
  = x4 or x3 = x5 or x3 = x6;
  then
A3: x4 in { x1, x2, x3 } or x5 in { x1, x2, x3 } or x6 in { x1, x2, x3 } by
ENUMSET1:def 1;
A4: x6 in { x4, x5, x6 } by ENUMSET1:def 1;
  x4 in { x4, x5, x6 } by ENUMSET1:def 1;
  hence thesis by A1,A3,A2,A4,XBOOLE_0:3;
end;

theorem
  x1, x2, x3 are_mutually_distinct & x4, x5, x6 are_mutually_distinct
  & { x1, x2, x3 } misses { x4, x5, x6 } implies x1, x2, x3, x4, x5, x6
  are_mutually_distinct
proof
  assume that
A1: x1, x2, x3 are_mutually_distinct and
A2: x4, x5, x6 are_mutually_distinct and
A3: { x1, x2, x3 } misses { x4, x5, x6 };
A4: x1 <> x2 by A1,ZFMISC_1:def 5;
A5: x3 <> x5 by A3,Th4;
A6: x3 <> x4 by A3,Th4;
A7: x1 <> x6 by A3,Th4;
A8: x1 <> x3 by A1,ZFMISC_1:def 5;
A9: x2 <> x5 by A3,Th4;
A10: x5 <> x6 by A2,ZFMISC_1:def 5;
A11: x2 <> x4 by A3,Th4;
A12: x4 <> x5 by A2,ZFMISC_1:def 5;
A13: x2 <> x6 by A3,Th4;
A14: x4 <> x6 by A2,ZFMISC_1:def 5;
A15: x3 <> x6 by A3,Th4;
A16: x1 <> x5 by A3,Th4;
A17: x2 <> x3 by A1,ZFMISC_1:def 5;
  x1 <> x4 by A3,Th4;
  hence thesis by A4,A17,A8,A12,A10,A14,A16,A7,A11,A9,A13,A6,A5,A15,
ZFMISC_1:def 8;
end;

theorem
  x1, x2, x3, x4, x5, x6 are_mutually_distinct & { x1, x2, x3, x4, x5,
  x6 } misses { x7 } implies x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct
proof
  assume that
A1: x1, x2, x3, x4, x5, x6 are_mutually_distinct and
A2: { x1, x2, x3, x4, x5, x6 } misses { x7 };
A3: x1 <> x3 by A1,ZFMISC_1:def 8;
A4: x2 <> x3 by A1,ZFMISC_1:def 8;
A5: x1 <> x6 by A1,ZFMISC_1:def 8;
A6: x1 <> x5 by A1,ZFMISC_1:def 8;
A7: x1 <> x4 by A1,ZFMISC_1:def 8;
A8: not x7 in { x1, x2, x3, x4, x5, x6 } by A2,ZFMISC_1:48;
  then
A9: x7 <> x1 by ENUMSET1:def 4;
A10: x4 <> x6 by A1,ZFMISC_1:def 8;
A11: x4 <> x5 by A1,ZFMISC_1:def 8;
A12: x3 <> x6 by A1,ZFMISC_1:def 8;
A13: x3 <> x5 by A1,ZFMISC_1:def 8;
A14: x3 <> x4 by A1,ZFMISC_1:def 8;
A15: x2 <> x6 by A1,ZFMISC_1:def 8;
A16: x2 <> x5 by A1,ZFMISC_1:def 8;
A17: x2 <> x4 by A1,ZFMISC_1:def 8;
A18: x7 <> x6 by A8,ENUMSET1:def 4;
A19: x5 <> x6 by A1,ZFMISC_1:def 8;
A20: x7 <> x5 by A8,ENUMSET1:def 4;
A21: x7 <> x4 by A8,ENUMSET1:def 4;
A22: x7 <> x3 by A8,ENUMSET1:def 4;
A23: x7 <> x2 by A8,ENUMSET1:def 4;
  x1 <> x2 by A1,ZFMISC_1:def 8;
  hence thesis by A3,A7,A6,A5,A4,A17,A16,A15,A14,A13,A12,A11,A10,A19,A9,A23,A22
,A21,A20,A18,ZFMISC_1:def 9;
end;

theorem
  x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct implies x7, x1, x2,
  x3, x4, x5, x6 are_mutually_distinct
proof
  assume
A1: x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct;
  then
A2: x1 <> x3 by ZFMISC_1:def 9;
A3: x5 <> x7 by A1,ZFMISC_1:def 9;
A4: x5 <> x6 by A1,ZFMISC_1:def 9;
A5: x4 <> x7 by A1,ZFMISC_1:def 9;
A6: x4 <> x6 by A1,ZFMISC_1:def 9;
A7: x6 <> x7 by A1,ZFMISC_1:def 9;
A8: x1 <> x5 by A1,ZFMISC_1:def 9;
A9: x1 <> x4 by A1,ZFMISC_1:def 9;
A10: x2 <> x4 by A1,ZFMISC_1:def 9;
A11: x2 <> x3 by A1,ZFMISC_1:def 9;
A12: x1 <> x7 by A1,ZFMISC_1:def 9;
A13: x1 <> x6 by A1,ZFMISC_1:def 9;
A14: x4 <> x5 by A1,ZFMISC_1:def 9;
A15: x3 <> x7 by A1,ZFMISC_1:def 9;
A16: x3 <> x6 by A1,ZFMISC_1:def 9;
A17: x3 <> x5 by A1,ZFMISC_1:def 9;
A18: x3 <> x4 by A1,ZFMISC_1:def 9;
A19: x2 <> x7 by A1,ZFMISC_1:def 9;
A20: x2 <> x6 by A1,ZFMISC_1:def 9;
A21: x2 <> x5 by A1,ZFMISC_1:def 9;
  x1 <> x2 by A1,ZFMISC_1:def 9;
  hence thesis by A2,A9,A8,A13,A12,A11,A10,A21,A20,A19,A18,A17,A16,A15,A14,A6
,A5,A4,A3,A7,ZFMISC_1:def 9;
end;

theorem
  x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct implies x1, x2, x5,
  x3, x6, x7, x4 are_mutually_distinct
proof
  assume
A1: x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct;
  then
A2: x1 <> x3 by ZFMISC_1:def 9;
A3: x5 <> x7 by A1,ZFMISC_1:def 9;
A4: x5 <> x6 by A1,ZFMISC_1:def 9;
A5: x4 <> x7 by A1,ZFMISC_1:def 9;
A6: x4 <> x6 by A1,ZFMISC_1:def 9;
A7: x6 <> x7 by A1,ZFMISC_1:def 9;
A8: x1 <> x5 by A1,ZFMISC_1:def 9;
A9: x1 <> x4 by A1,ZFMISC_1:def 9;
A10: x2 <> x4 by A1,ZFMISC_1:def 9;
A11: x2 <> x3 by A1,ZFMISC_1:def 9;
A12: x1 <> x7 by A1,ZFMISC_1:def 9;
A13: x1 <> x6 by A1,ZFMISC_1:def 9;
A14: x4 <> x5 by A1,ZFMISC_1:def 9;
A15: x3 <> x7 by A1,ZFMISC_1:def 9;
A16: x3 <> x6 by A1,ZFMISC_1:def 9;
A17: x3 <> x5 by A1,ZFMISC_1:def 9;
A18: x3 <> x4 by A1,ZFMISC_1:def 9;
A19: x2 <> x7 by A1,ZFMISC_1:def 9;
A20: x2 <> x6 by A1,ZFMISC_1:def 9;
A21: x2 <> x5 by A1,ZFMISC_1:def 9;
  x1 <> x2 by A1,ZFMISC_1:def 9;
  hence thesis by A2,A9,A8,A13,A12,A11,A10,A21,A20,A19,A18,A17,A16,A15,A14,A6
,A5,A4,A3,A7,ZFMISC_1:def 9;
end;

Lm1: R^1 is pathwise_connected
proof
  let a, b be Point of R^1;
  per cases;
  suppose
A1: a <= b;
    reconsider B = [. a, b .] as Subset of R^1 by TOPMETR:17;
    reconsider B as non empty Subset of R^1 by A1,XXREAL_1:1;
A2: Closed-Interval-TSpace(a,b) = R^1|B by A1,TOPMETR:19;
    the carrier of R^1|B c= the carrier of R^1 by BORSUK_1:1;
    then reconsider g = L[01]((#)(a,b),(a,b)(#)) as Function of the carrier of
    I[01], the carrier of R^1 by A2,FUNCT_2:7,TOPMETR:20;
    reconsider g as Function of I[01], R^1;
    take g;
    L[01]((#)(a,b),(a,b)(#)) is continuous Function of I[01], R^1|B by A1,A2,
TOPMETR:20,TREAL_1:8;
    hence g is continuous by PRE_TOPC:26;
    0 = (#)(0,1) by TREAL_1:def 1;
    hence g.0 = (#)(a,b) by A1,TREAL_1:9
      .= a by A1,TREAL_1:def 1;
    1 = (0,1)(#) by TREAL_1:def 2;
    hence g.1 = (a,b)(#) by A1,TREAL_1:9
      .= b by A1,TREAL_1:def 2;
  end;
  suppose
A3: b <= a;
    reconsider B = [. b, a .] as Subset of R^1 by TOPMETR:17;
    b in B by A3,XXREAL_1:1;
    then reconsider B = [. b, a .] as non empty Subset of R^1;
A4: Closed-Interval-TSpace(b,a) = R^1|B by A3,TOPMETR:19;
    the carrier of R^1|B c= the carrier of R^1 by BORSUK_1:1;
    then reconsider g = L[01]((#)(b,a),(b,a)(#)) as Function of the carrier of
    I[01], the carrier of R^1 by A4,FUNCT_2:7,TOPMETR:20;
    reconsider g as Function of I[01], R^1;
    0 = (#)(0,1) by TREAL_1:def 1;
    then
A5: g.0 = (#)(b,a) by A3,TREAL_1:9
      .= b by A3,TREAL_1:def 1;
    1 = (0,1)(#) by TREAL_1:def 2;
    then
A6: g.1 = (b,a)(#) by A3,TREAL_1:9
      .= a by A3,TREAL_1:def 2;
    L[01]((#)(b,a),(b,a)(#)) is continuous Function of I[01], R^1|B by A3,A4,
TOPMETR:20,TREAL_1:8;
    then
A7: g is continuous by PRE_TOPC:26;
    then b,a are_connected by A5,A6;
    then reconsider P = g as Path of b, a by A7,A5,A6,BORSUK_2:def 2;
    take -P;
    ex t being Function of I[01], R^1 st t is continuous & t.0 = a & t.1
    = b by A7,A5,A6,BORSUK_2:15;
    then a,b are_connected;
    hence thesis by BORSUK_2:def 2;
  end;
end;

registration
  cluster R^1 -> pathwise_connected;
  coherence by Lm1;
end;

registration
  cluster connected non empty for TopSpace;
  existence
  proof
    take R^1;
    thus thesis;
  end;
end;

begin :: Intervals

theorem
  for A, B being Subset of R^1, a, b, c, d being Real st a < b &
  b <= c & c < d & A = [. a, b .[ & B = ]. c, d .] holds A, B are_separated
proof
  let A, B be Subset of R^1, a, b, c, d be Real;
  assume that
A1: a < b and
A2: b <= c and
A3: c < d and
A4: A = [. a, b .[ and
A5: B = ]. c, d .];
  Cl ]. c, d .] = [. c, d .] by A3,BORSUK_4:11;
  then Cl B = [. c, d .] by A5,JORDAN5A:24;
  then
A6: Cl B misses A by A2,A4,XXREAL_1:95;
  Cl [. a, b .[ = [. a, b .] by A1,BORSUK_4:12;
  then Cl A = [. a, b .] by A4,JORDAN5A:24;
  then Cl A misses B by A2,A5,XXREAL_1:90;
  hence thesis by A6,CONNSP_1:def 1;
end;

theorem Th10:
  for a, b, c being Real st a <= c & c <= b holds [.a,b.]
  \/ [.c,+infty .[ = [.a,+infty .[
proof
  let a, b, c be Real;
  assume that
A1: a <= c and
A2: c <= b;
A3: [.a,+infty .[ c= [.a,b.] \/ [.c,+infty .[
  proof
    let r be object;
    assume
A4: r in [.a,+infty .[;
    then reconsider s = r as Real;
A5: a <= s by A4,XXREAL_1:236;
    per cases;
    suppose
      s <= b;
      then s in [.a,b.] by A5,XXREAL_1:1;
      hence thesis by XBOOLE_0:def 3;
    end;
    suppose
      not s <= b;
      then c <= s by A2,XXREAL_0:2;
      then s in [.c,+infty .[ by XXREAL_1:236;
      hence thesis by XBOOLE_0:def 3;
    end;
  end;
A6: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
  [.c,+infty .[ c= [.a,+infty .[ by A1,XXREAL_1:38;
  then [.a,b.] \/ [.c,+infty .[ c= [.a,+infty .[ by A6,XBOOLE_1:8;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem Th11:
  for a, b, c being Real st a <= c & c <= b holds ]. -infty
  , c .] \/ [. a, b .] = ]. -infty, b .]
proof
  let a, b, c be Real;
  assume that
A1: a <= c and
A2: c <= b;
  thus ]. -infty, c .] \/ [. a, b .] c= ]. -infty, b .]
  proof
    let x be object;
    assume
A3: x in ]. -infty, c .] \/ [. a, b .];
    then reconsider x as Real;
    per cases by A3,XBOOLE_0:def 3;
    suppose
      x in ]. -infty, c .];
      then x <= c by XXREAL_1:234;
      then x <= b by A2,XXREAL_0:2;
      hence thesis by XXREAL_1:234;
    end;
    suppose
      x in [. a, b .];
      then x <= b by XXREAL_1:1;
      hence thesis by XXREAL_1:234;
    end;
  end;
  let x be object;
  assume
A4: x in ]. -infty, b .];
  then reconsider x as Real;
  per cases;
  suppose
    x <= c;
    then x in ]. -infty, c .] by XXREAL_1:234;
    hence thesis by XBOOLE_0:def 3;
  end;
  suppose
A5: x > c;
A6: x <= b by A4,XXREAL_1:234;
    x > a by A1,A5,XXREAL_0:2;
    then x in [. a, b .] by A6,XXREAL_1:1;
    hence thesis by XBOOLE_0:def 3;
  end;
end;

registration
  cluster -> real for Element of RAT;
  coherence;
end;

theorem
  for A being Subset of R^1, p being Point of RealSpace holds p in Cl A
iff for r being Real st r > 0 holds Ball (p, r) meets A by GOBOARD6:92
,TOPMETR:def 6;

theorem Th13:
  for p, q being Element of RealSpace st q >= p holds dist (p, q) = q - p
proof
  let p, q be Element of RealSpace;
  assume p <= q;
  then
A1: q - p >= 0 by XREAL_1:48;
  dist (p, q) = |.q - p.| by TOPMETR:11
    .= q - p by A1,ABSVALUE:def 1;
  hence thesis;
end;

theorem Th14:
  for A being Subset of R^1 st A = RAT holds Cl A = the carrier of R^1
proof
  let A be Subset of R^1;
  assume
A1: A = RAT;
  the carrier of R^1 c= Cl A
  proof
    let x be object;
    assume x in the carrier of R^1;
    then reconsider p = x as Element of RealSpace by METRIC_1:def 13,TOPMETR:17
;
    now
      let r be Real;
      reconsider pr = p + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
      assume r > 0;
      then consider Q being Rational such that
A2:   p < Q and
A3:   Q < pr by RAT_1:7,XREAL_1:29;
      reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
      P - p < pr - p by A3,XREAL_1:9;
      then dist (p, P) < r by A2,Th13;
      then
A4:   P in Ball (p, r) by METRIC_1:11;
      Q in A by A1,RAT_1:def 2;
      hence Ball (p, r) meets A by A4,XBOOLE_0:3;
    end;
    hence thesis by GOBOARD6:92,TOPMETR:def 6;
  end;
  hence thesis by XBOOLE_0:def 10;
end;

theorem Th15:
  for A being Subset of R^1, a, b being Real st A = ]. a, b
  .[ & a <> b holds Cl A = [. a, b .]
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: A = ]. a, b .[ and
A2: a <> b;
  Cl ]. a, b .[ = [. a, b .] by A2,JORDAN5A:26;
  hence thesis by A1,JORDAN5A:24;
end;

begin :: Rational and Irrational Numbers

registration
  cluster number_e -> irrational;
  coherence by IRRAT_1:41;
end;

definition
  func IRRAT -> Subset of REAL equals
  REAL \ RAT;
  coherence;
end;

definition
  let a, b be Real;
  func RAT (a, b) -> Subset of REAL equals
  RAT /\ ]. a, b .[;
  coherence;
  func IRRAT (a, b) -> Subset of REAL equals
  IRRAT /\ ]. a, b .[;
  coherence;
end;

theorem Th16:
  for x being Real holds x is irrational iff x in IRRAT
proof
  let x be Real;
A1: x in REAL by XREAL_0:def 1;
  hereby
    assume x is irrational;
    then not x in RAT;
    hence x in IRRAT by A1,XBOOLE_0:def 5;
  end;
  assume x in IRRAT;
  then not x in RAT by XBOOLE_0:def 5;
  hence thesis by RAT_1:def 2;
end;

registration
  cluster irrational for Real;
  existence by IRRAT_1:41;
end;

registration
  cluster IRRAT -> non empty;
  coherence by Th16,IRRAT_1:41;
end;

registration
  let a be Rational, b be irrational Real;
  cluster a + b -> irrational;
  coherence
proof
  set m1 = the Integer;
  assume a + b is rational;
  then consider m, n being Integer such that
  n <> 0 and
A1: a + b = m / n by RAT_1:2;
  a + b - a = (m*m1 - m1*n) / (m1*n) by A1;
  hence thesis;
end;
  cluster b + a -> irrational;
  coherence;
end;

theorem
  for a being Rational, b being irrational Real
  holds a + b is irrational;

registration
  let a be irrational Real;
  cluster -a -> irrational;
  coherence
proof
  assume -a is rational;
  then reconsider b = -a as Rational;
  -b is rational;
  hence thesis;
end;
end;

theorem
  for a being irrational Real holds -a is irrational;

registration
  let a be Rational, b be irrational Real;
  cluster a - b -> irrational;
  coherence
proof
  a + -b is irrational;
  hence thesis;
end;
  cluster b - a -> irrational;
  coherence
proof
  b + -a is irrational;
  hence thesis;
end;
end;

theorem
  for a being Rational, b being irrational Real
  holds a - b is irrational;

theorem
  for a being Rational, b being irrational Real
  holds b - a is irrational;

theorem Th21:
  for a being Rational, b being irrational Real st
  a <> 0 holds a * b is irrational
proof
  let a be Rational, b be irrational Real;
  assume
A1: a <> 0;
  assume a * b is rational;
  then consider m, n being Integer such that
  n <> 0 and
A2: a * b = m / n by RAT_1:2;
  consider m1, n1 being Integer such that
  n1 <> 0 and
A3: a = m1 / n1 by RAT_1:2;
  a * b / a = (m * n1) / (n * m1) by A2,A3,XCMPLX_1:84;
  hence thesis by A1,XCMPLX_1:89;
end;

theorem Th22:
  for a being Rational, b being irrational Real st
  a <> 0 holds b / a is irrational
proof
  let a be Rational, b be irrational Real;
  assume
A1: a <> 0;
  assume b / a is rational;
  then reconsider c = b / a as Rational;
  c * a is rational;
  hence thesis by A1,XCMPLX_1:87;
end;

registration
  cluster irrational -> non zero for Real;
  coherence;
end;

theorem Th23:
  for a being Rational, b being irrational Real st
  a <> 0 holds a / b is irrational
proof
  let a be Rational, b be irrational Real;
  assume
A1: a <> 0;
  assume a / b is rational;
  then reconsider c = a / b as Rational;
  c * b is irrational by A1,Th21,XCMPLX_1:50;
  hence thesis by XCMPLX_1:87;
end;

registration
  let r be irrational Real;
  cluster frac r -> irrational;
  coherence
proof
  frac r = r - [\ r /] by INT_1:def 8;
  hence thesis;
end;
end;

theorem
  for r being irrational Real holds frac r is irrational;

registration
  cluster non zero for Rational;
  existence
  proof
    1 <> 0;
    hence thesis;
  end;
end;

registration
  let a be non zero Rational, b be irrational Real;
  cluster a * b -> irrational;
  coherence by Th21;
  cluster b * a -> irrational;
  coherence;
  cluster a / b -> irrational;
  coherence by Th23;
  cluster b / a -> irrational;
  coherence by Th22;
end;

theorem Th25:
  for a, b being Real st a < b ex p1, p2 being Rational
 st a < p1 & p1 < p2 & p2 < b
proof
  let a, b be Real;
  assume a < b;
  then consider p1 being Rational such that
A1: a < p1 and
A2: p1 < b by RAT_1:7;
  ex p2 being Rational st p1 < p2 & p2 < b by A2,RAT_1:7;
  hence thesis by A1;
end;

theorem Th26:
  for a, b being Real st a < b ex p being irrational Real st a < p & p < b
proof
  set x = frac number_e;
  let a, b be Real;
A1: x < 1 by INT_1:43;
  assume a < b;
  then consider p1, p2 being Rational such that
A2: a < p1 and
A3: p1 < p2 and
A4: p2 < b by Th25;
  set y = (1 - x) * p1 + x * p2;
A5: 0 < x by INT_1:43;
  then y < p2 by A3,A1,XREAL_1:178;
  then
A6: y < b by A4,XXREAL_0:2;
  y > p1 by A3,A5,A1,XREAL_1:177;
  then
A7: y > a by A2,XXREAL_0:2;
A8: y = p1 + x * (p2 - p1);
  p2 - p1 <> 0 by A3;
  hence thesis by A8,A6,A7;
end;

theorem Th27:
  for A being Subset of R^1 st A = IRRAT holds Cl A = the carrier of R^1
proof
  let A be Subset of R^1;
  assume
A1: A = IRRAT;
  the carrier of R^1 c= Cl A
  proof
    let x be object;
    assume x in the carrier of R^1;
    then reconsider p = x as Element of RealSpace by METRIC_1:def 13,TOPMETR:17
;
    now
      let r be Real;
      reconsider pr = p + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
      assume r > 0;
      then consider Q being irrational Real such that
A2:   p < Q and
A3:   Q < pr by Th26,XREAL_1:29;
      reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
      P - p < pr - p by A3,XREAL_1:9;
      then dist (p, P) < r by A2,Th13;
      then
A4:   P in Ball (p, r) by METRIC_1:11;
      Q in A by A1,Th16;
      hence Ball (p, r) meets A by A4,XBOOLE_0:3;
    end;
    hence thesis by GOBOARD6:92,TOPMETR:def 6;
  end;
  hence thesis by XBOOLE_0:def 10;
end;

Lm2: for A being Subset of R^1, a, b being Real st a < b & A = RAT (a,
b) holds a in Cl A & b in Cl A
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a < b and
A2: A = RAT (a, b);
  thus a in Cl A
  proof
    reconsider a9 = a as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
    for r being Real st r > 0 holds Ball (a9, r) meets A
    proof
      set p = a;
      let r be Real;
      reconsider pp = a + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
      set pr = min (pp, (p + b)/2);
A3:   pr <= (p + b)/2 by XXREAL_0:17;
      assume
A4:   r > 0;
      p < pr
      proof
        per cases by XXREAL_0:15;
        suppose
          pr = pp;
          hence thesis by A4,XREAL_1:29;
        end;
        suppose
          pr = (p + b)/2;
          hence thesis by A1,XREAL_1:226;
        end;
      end;
      then consider Q being Rational such that
A5:   p < Q and
A6:   Q < pr by RAT_1:7;
      (p + b)/2 < b by A1,XREAL_1:226;
      then pr < b by A3,XXREAL_0:2;
      then Q < b by A6,XXREAL_0:2;
      then
A7:   Q in ]. a, b .[ by A5,XXREAL_1:4;
      pr <= pp by XXREAL_0:17;
      then
A8:   pr - p <= pp - p by XREAL_1:9;
      reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
      P - p < pr - p by A6,XREAL_1:9;
      then P - p < r by A8,XXREAL_0:2;
      then dist (a9, P) < r by A5,Th13;
      then
A9:   P in Ball (a9, r) by METRIC_1:11;
      Q in RAT by RAT_1:def 2;
      then Q in A by A2,A7,XBOOLE_0:def 4;
      hence thesis by A9,XBOOLE_0:3;
    end;
    hence thesis by GOBOARD6:92,TOPMETR:def 6;
  end;
  b in Cl A
  proof
    reconsider a9 = b as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
    for r being Real st r > 0 holds Ball (a9, r) meets A
    proof
      set p = b;
      let r be Real;
      reconsider pp = b - r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
      set pr = max (pp, (p + a)/2);
A10:  pr >= (p + a)/2 by XXREAL_0:25;
      assume r > 0;
      then
A11:  b < b + r by XREAL_1:29;
      p > pr
      proof
        per cases by XXREAL_0:16;
        suppose
          pr = pp;
          hence thesis by A11,XREAL_1:19;
        end;
        suppose
          pr = (p + a)/2;
          hence thesis by A1,XREAL_1:226;
        end;
      end;
      then consider Q being Rational such that
A12:  pr < Q and
A13:  Q < p by RAT_1:7;
      (p + a)/2 > a by A1,XREAL_1:226;
      then a < pr by A10,XXREAL_0:2;
      then a < Q by A12,XXREAL_0:2;
      then
A14:  Q in ]. a, b .[ by A13,XXREAL_1:4;
      pr >= pp by XXREAL_0:25;
      then
A15:  p - pr <= p - pp by XREAL_1:13;
      reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
      p - P < p - pr by A12,XREAL_1:10;
      then p - P < r by A15,XXREAL_0:2;
      then dist (a9, P) < r by A13,Th13;
      then
A16:  P in Ball (a9, r) by METRIC_1:11;
      Q in RAT by RAT_1:def 2;
      then Q in A by A2,A14,XBOOLE_0:def 4;
      hence thesis by A16,XBOOLE_0:3;
    end;
    hence thesis by GOBOARD6:92,TOPMETR:def 6;
  end;
  hence thesis;
end;

Lm3: for A being Subset of R^1, a, b being Real st a < b & A = IRRAT (a
, b) holds a in Cl A & b in Cl A
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a < b and
A2: A = IRRAT (a, b);
  thus a in Cl A
  proof
    reconsider a9 = a as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
    for r being Real st r > 0 holds Ball (a9, r) meets A
    proof
      set p = a;
      let r be Real;
      reconsider pp = a + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
      set pr = min (pp, (p + b)/2);
A3:   pr <= (p + b)/2 by XXREAL_0:17;
      assume
A4:   r > 0;
      p < pr
      proof
        per cases by XXREAL_0:15;
        suppose
          pr = pp;
          hence thesis by A4,XREAL_1:29;
        end;
        suppose
          pr = (p + b)/2;
          hence thesis by A1,XREAL_1:226;
        end;
      end;
      then consider Q being irrational Real such that
A5:   p < Q and
A6:   Q < pr by Th26;
      (p + b)/2 < b by A1,XREAL_1:226;
      then pr < b by A3,XXREAL_0:2;
      then Q < b by A6,XXREAL_0:2;
      then
A7:   Q in ]. a, b .[ by A5,XXREAL_1:4;
      pr <= pp by XXREAL_0:17;
      then
A8:   pr - p <= pp - p by XREAL_1:9;
      reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
      P - p < pr - p by A6,XREAL_1:9;
      then P - p < r by A8,XXREAL_0:2;
      then dist (a9, P) < r by A5,Th13;
      then
A9:   P in Ball (a9, r) by METRIC_1:11;
      Q in IRRAT by Th16;
      then Q in A by A2,A7,XBOOLE_0:def 4;
      hence thesis by A9,XBOOLE_0:3;
    end;
    hence thesis by GOBOARD6:92,TOPMETR:def 6;
  end;
  b in Cl A
  proof
    reconsider a9 = b as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
    for r being Real st r > 0 holds Ball (a9, r) meets A
    proof
      set p = b;
      let r be Real;
      reconsider pp = b - r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
      set pr = max (pp, (p + a)/2);
A10:  pr >= (p + a)/2 by XXREAL_0:25;
      assume r > 0;
      then
A11:  b < b + r by XREAL_1:29;
      p > pr
      proof
        per cases by XXREAL_0:16;
        suppose
          pr = pp;
          hence thesis by A11,XREAL_1:19;
        end;
        suppose
          pr = (p + a)/2;
          hence thesis by A1,XREAL_1:226;
        end;
      end;
      then consider Q being irrational Real such that
A12:  pr < Q and
A13:  Q < p by Th26;
      (p + a)/2 > a by A1,XREAL_1:226;
      then a < pr by A10,XXREAL_0:2;
      then a < Q by A12,XXREAL_0:2;
      then
A14:  Q in ]. a, b .[ by A13,XXREAL_1:4;
      pr >= pp by XXREAL_0:25;
      then
A15:  p - pr <= p - pp by XREAL_1:13;
      reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
      p - P < p - pr by A12,XREAL_1:10;
      then p - P < r by A15,XXREAL_0:2;
      then dist (a9, P) < r by A13,Th13;
      then
A16:  P in Ball (a9, r) by METRIC_1:11;
      Q in IRRAT by Th16;
      then Q in A by A2,A14,XBOOLE_0:def 4;
      hence thesis by A16,XBOOLE_0:3;
    end;
    hence thesis by GOBOARD6:92,TOPMETR:def 6;
  end;
  hence thesis;
end;

theorem Th28:
  for a, b, c being Real holds c in RAT (a,b) iff c is
  rational & a < c & c < b
proof
  let a, b, c be Real;
  hereby
    assume
A1: c in RAT (a,b);
    then c in ]. a, b .[ by XBOOLE_0:def 4;
    hence c is rational & a < c & c < b by A1,XXREAL_1:4;
  end;
  assume that
A2: c is rational and
A3: a < c and
A4: c < b;
A5: c in RAT by A2,RAT_1:def 2;
  c in ]. a, b .[ by A3,A4,XXREAL_1:4;
  hence thesis by A5,XBOOLE_0:def 4;
end;

theorem Th29:
  for a, b, c being Real holds c in IRRAT (a,b) iff c is
  irrational & a < c & c < b
proof
  let a, b, c be Real;
  hereby
    assume
A1: c in IRRAT (a,b);
    then
A2: c in ]. a, b .[ by XBOOLE_0:def 4;
    c in IRRAT by A1,XBOOLE_0:def 4;
    hence c is irrational & a < c & c < b by A2,Th16,XXREAL_1:4;
  end;
  assume that
A3: c is irrational and
A4: a < c and
A5: c < b;
A6: c in ]. a, b .[ by A4,A5,XXREAL_1:4;
  c in IRRAT by A3,Th16;
  hence thesis by A6,XBOOLE_0:def 4;
end;

theorem Th30:
  for A being Subset of R^1, a, b being Real st a < b & A =
  RAT (a, b) holds Cl A = [. a, b .]
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a < b and
A2: A = RAT (a, b);
  reconsider ab = ]. a, b .[, RT = RAT as Subset of R^1 by NUMBERS:12
,TOPMETR:17;
  reconsider RR = RAT /\ ]. a, b .[ as Subset of R^1 by TOPMETR:17;
A3: (the carrier of R^1) /\ Cl ab = Cl ab by XBOOLE_1:28;
A4: Cl RR c= (Cl RT) /\ Cl ab by PRE_TOPC:21;
  thus Cl A c= [. a, b .]
  proof
    let x be object;
    assume x in Cl A;
    then x in (Cl RT) /\ Cl ab by A2,A4;
    then x in (the carrier of R^1) /\ Cl ab by Th14;
    hence thesis by A1,A3,Th15;
  end;
  thus [. a, b .] c= Cl A
  proof
    let x be object;
    assume
A5: x in [. a, b .];
    then reconsider p = x as Element of RealSpace by METRIC_1:def 13;
A6: a <= p by A5,XXREAL_1:1;
A7: p <= b by A5,XXREAL_1:1;
    per cases by A7,XXREAL_0:1;
    suppose
A8:   p < b;
      now
        let r be Real;
        reconsider pp = p + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
        set pr = min (pp, (p + b)/2);
A9:     pr <= (p + b)/2 by XXREAL_0:17;
        assume
A10:    r > 0;
        p < pr
        proof
          per cases by XXREAL_0:15;
          suppose
            pr = pp;
            hence thesis by A10,XREAL_1:29;
          end;
          suppose
            pr = (p + b)/2;
            hence thesis by A8,XREAL_1:226;
          end;
        end;
        then consider Q being Rational such that
A11:    p < Q and
A12:    Q < pr by RAT_1:7;
        (p + b)/2 < b by A8,XREAL_1:226;
        then pr < b by A9,XXREAL_0:2;
        then
A13:    Q < b by A12,XXREAL_0:2;
        pr <= pp by XXREAL_0:17;
        then
A14:    pr - p <= pp - p by XREAL_1:9;
        reconsider P = Q as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
        P - p < pr - p by A12,XREAL_1:9;
        then P - p < r by A14,XXREAL_0:2;
        then dist (p, P) < r by A11,Th13;
        then
A15:    P in Ball (p, r) by METRIC_1:11;
        a < Q by A6,A11,XXREAL_0:2;
        then
A16:    Q in ]. a, b .[ by A13,XXREAL_1:4;
        Q in RAT by RAT_1:def 2;
        then Q in A by A2,A16,XBOOLE_0:def 4;
        hence Ball (p, r) meets A by A15,XBOOLE_0:3;
      end;
      hence thesis by GOBOARD6:92,TOPMETR:def 6;
    end;
    suppose
      p = b;
      hence thesis by A1,A2,Lm2;
    end;
  end;
end;

theorem Th31:
  for A being Subset of R^1, a, b being Real st a < b & A =
  IRRAT (a, b) holds Cl A = [. a, b .]
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a < b and
A2: A = IRRAT (a, b);
  reconsider ab = ]. a, b .[, RT = IRRAT as Subset of R^1 by TOPMETR:17;
  reconsider RR = IRRAT /\ ]. a, b .[ as Subset of R^1 by TOPMETR:17;
A3: (the carrier of R^1) /\ Cl ab = Cl ab by XBOOLE_1:28;
A4: Cl RR c= (Cl RT) /\ Cl ab by PRE_TOPC:21;
  thus Cl A c= [. a, b .]
  proof
    let x be object;
    assume x in Cl A;
    then x in (Cl RT) /\ Cl ab by A2,A4;
    then x in (the carrier of R^1) /\ Cl ab by Th27;
    hence thesis by A1,A3,Th15;
  end;
  thus [. a, b .] c= Cl A
  proof
    let x be object;
    assume
A5: x in [. a, b .];
    then reconsider p = x as Element of RealSpace by METRIC_1:def 13;
A6: a <= p by A5,XXREAL_1:1;
A7: p <= b by A5,XXREAL_1:1;
    per cases by A7,XXREAL_0:1;
    suppose
A8:   p < b;
      now
        let r be Real;
        reconsider pp = p + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
        set pr = min (pp, (p + b)/2);
A9:     pr <= (p + b)/2 by XXREAL_0:17;
        assume
A10:    r > 0;
        p < pr
        proof
          per cases by XXREAL_0:15;
          suppose
            pr = pp;
            hence thesis by A10,XREAL_1:29;
          end;
          suppose
            pr = (p + b)/2;
            hence thesis by A8,XREAL_1:226;
          end;
        end;
        then consider Q being irrational Real such that
A11:    p < Q and
A12:    Q < pr by Th26;
        (p + b)/2 < b by A8,XREAL_1:226;
        then pr < b by A9,XXREAL_0:2;
        then
A13:    Q < b by A12,XXREAL_0:2;
        pr <= pp by XXREAL_0:17;
        then
A14:    pr - p <= pp - p by XREAL_1:9;
        reconsider P = Q as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
        P - p < pr - p by A12,XREAL_1:9;
        then P - p < r by A14,XXREAL_0:2;
        then dist (p, P) < r by A11,Th13;
        then
A15:    P in Ball (p, r) by METRIC_1:11;
        a < Q by A6,A11,XXREAL_0:2;
        then
A16:    Q in ]. a, b .[ by A13,XXREAL_1:4;
        Q in IRRAT by Th16;
        then Q in A by A2,A16,XBOOLE_0:def 4;
        hence Ball (p, r) meets A by A15,XBOOLE_0:3;
      end;
      hence thesis by GOBOARD6:92,TOPMETR:def 6;
    end;
    suppose
      p = b;
      hence thesis by A1,A2,Lm3;
    end;
  end;
end;

theorem Th32:
  for T being connected TopSpace, A being closed open Subset of T
  holds A = {} or A = [#]T
proof
  let T be connected TopSpace, A be closed open Subset of T;
  assume that
A1: A <> {} and
A2: A <> [#]T;
A3: A` <> {} by A2,PRE_TOPC:4;
  A misses A` by SUBSET_1:24;
  then
A4: A, A` are_separated by CONNSP_1:2;
A5: [#]T = A \/ A` by PRE_TOPC:2;
  A <> {}T by A1;
  then not [#]T is connected by A5,A4,A3,CONNSP_1:15;
  hence thesis by CONNSP_1:27;
end;

theorem Th33:
  for A being Subset of R^1 st A is closed open holds A = {} or A = REAL
proof
  let A be Subset of R^1;
  assume A is closed open;
  then reconsider A as closed open Subset of R^1;
  A = {} or A = [#]R^1 by Th32;
  hence thesis by TOPMETR:17;
end;

begin :: Topological Properties of Intervals

theorem Th34:
  for A being Subset of R^1, a, b being Real st A = [. a, b
  .[ & a <> b holds Cl A = [. a, b .]
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: A = [. a, b .[ and
A2: a <> b;
  Cl [. a, b .[ = [. a, b .] by A2,BORSUK_4:12;
  hence thesis by A1,JORDAN5A:24;
end;

theorem Th35:
  for A being Subset of R^1, a, b being Real st A = ]. a, b
  .] & a <> b holds Cl A = [. a, b .]
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: A = ]. a, b .] and
A2: a <> b;
  Cl ]. a, b .] = [. a, b .] by A2,BORSUK_4:11;
  hence thesis by A1,JORDAN5A:24;
end;

theorem
  for A being Subset of R^1, a, b, c being Real st A = [. a, b .[
  \/ ]. b, c .] & a < b & b < c holds Cl A = [. a, c .]
proof
  let A be Subset of R^1, a, b, c be Real;
  assume that
A1: A = [. a, b .[ \/ ]. b, c .] and
A2: a < b and
A3: b < c;
  reconsider B = [. a, b .[, C = ]. b, c .] as Subset of R^1 by TOPMETR:17;
  Cl A = Cl B \/ Cl C by A1,PRE_TOPC:20
    .= [. a, b .] \/ Cl C by A2,Th34
    .= [. a, b .] \/ [. b, c .] by A3,Th35
    .= [. a, c .] by A2,A3,XXREAL_1:174;
  hence thesis;
end;

theorem Th37:
  for A being Subset of R^1, a being Real st A = {a} holds Cl A = {a}
proof
  let A be Subset of R^1, a be Real;
A1: a is Point of R^1 by TOPMETR:17,XREAL_0:def 1;
  assume A = {a};
  hence thesis by A1,YELLOW_8:26;
end;

theorem Th38:
  for A being Subset of REAL, B being Subset of R^1 st A = B holds
  A is open iff B is open
proof
  let A be Subset of REAL, B be Subset of R^1;
  assume
A1: A = B;
  hereby
    assume A is open;
    then A in Family_open_set RealSpace by JORDAN5A:5;
    then A in the topology of TopSpaceMetr RealSpace by TOPMETR:12;
    hence B is open by A1,PRE_TOPC:def 2,TOPMETR:def 6;
  end;
  assume B is open;
  then B in the topology of R^1 by PRE_TOPC:def 2;
  then A in Family_open_set RealSpace by A1,TOPMETR:12,def 6;
  hence thesis by JORDAN5A:5;
end;

Lm4: for a being Real holds ]. -infty,a.] is closed
proof
  let a be Real;
  ]. -infty,a.] = left_closed_halfline a;
  hence thesis;
end;

Lm5: for a being Real holds [.a,+infty .[ is closed
proof
  let a be Real;
  [. a,+infty .[ = right_closed_halfline a;
  hence thesis;
end;

registration
  let A, B be open Subset of REAL;
  reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17;
  cluster A /\ B -> open for Subset of REAL;
  coherence
  proof
A1: B1 is open by Th38;
    A1 is open by Th38;
    then A1 /\ B1 is open by A1;
    hence thesis by Th38;
  end;
  cluster A \/ B -> open for Subset of REAL;
  coherence
  proof
A2: B1 is open by Th38;
    A1 is open by Th38;
    then A1 \/ B1 is open by A2;
    hence thesis by Th38;
  end;
end;

Lm6: for a,b being ExtReal holds ]. a,b .[ is open
proof
  let a,b be ExtReal;
  set A = ]. a,b .[;
  per cases by XXREAL_0:14;
  suppose
    a in REAL & b in REAL;
    then reconsider a, b as Real;
    A = ].-infty,b.[ /\ ].a,+infty.[ by XXREAL_1:269;
    hence thesis;
  end;
  suppose
    a = +infty;
    then A = {} by XXREAL_1:214;
    hence thesis;
  end;
  suppose that
A1: a = -infty and
A2: b in REAL;
    reconsider b as Real by A2;
    A = left_open_halfline b by A1;
    hence thesis;
  end;
  suppose that
A3: a in REAL and
A4: b = +infty;
    reconsider a as Real by A3;
    A = right_open_halfline a by A4;
    hence thesis;
  end;
  suppose
    b = -infty;
    then A = {} by XXREAL_1:210;
    hence thesis;
  end;
  suppose
    a = -infty & b = +infty;
    then A = [#]REAL by XXREAL_1:224;
    hence thesis;
  end;
end;

theorem Th39:
  for A being Subset of R^1, a,b being ExtReal st A = ]. a
  ,b .[ holds A is open
proof
  let A be Subset of R^1, a,b be ExtReal;
  ]. a,b .[ is open by Lm6;
  hence thesis by Th38;
end;

theorem Th40:
  for A being Subset of R^1, a being Real st A = ]. -infty,
  a.] holds A is closed
proof
  let A be Subset of R^1, a be Real;
  assume
A1: A = ]. -infty,a.];
  ]. -infty,a.] is closed by Lm4;
  hence thesis by A1,JORDAN5A:23;
end;

theorem Th41:
  for A being Subset of R^1, a being Real st A = [. a,
  +infty .[ holds A is closed
proof
  let A be Subset of R^1, a be Real;
  assume
A1: A = [. a,+infty .[;
  [. a,+infty .[ is closed by Lm5;
  hence thesis by A1,JORDAN5A:23;
end;

theorem Th42:
  for a being Real holds [. a,+infty .[ = {a} \/ ]. a, +infty .[
proof
  let a be Real;
  thus [. a,+infty .[ c= {a} \/ ]. a,+infty .[
  proof
    let x be object;
    assume
A1: x in [. a,+infty .[;
    then reconsider x as Real;
A2: x >= a by A1,XXREAL_1:236;
    per cases by A2,XXREAL_0:1;
    suppose
      x = a;
      then x in {a} by TARSKI:def 1;
      hence thesis by XBOOLE_0:def 3;
    end;
    suppose
      x > a;
      then x in ]. a,+infty .[ by XXREAL_1:235;
      hence thesis by XBOOLE_0:def 3;
    end;
  end;
  let x be object;
  assume
A3: x in {a} \/ ]. a,+infty .[;
  then reconsider x as Real;
  x in {a} or x in ]. a,+infty .[ by A3,XBOOLE_0:def 3;
  then x = a or x > a by TARSKI:def 1,XXREAL_1:235;
  hence thesis by XXREAL_1:236;
end;

theorem Th43:
  for a being Real holds ]. -infty,a.] = {a} \/ ]. -infty,a .[
proof
  let a be Real;
  thus ]. -infty,a.] c= {a} \/ ]. -infty,a.[
  proof
    let x be object;
    assume
A1: x in ]. -infty,a.];
    then reconsider x as Real;
A2: x <= a by A1,XXREAL_1:234;
    per cases by A2,XXREAL_0:1;
    suppose
      x = a;
      then x in {a} by TARSKI:def 1;
      hence thesis by XBOOLE_0:def 3;
    end;
    suppose
      x < a;
      then x in ]. -infty,a.[ by XXREAL_1:233;
      hence thesis by XBOOLE_0:def 3;
    end;
  end;
  let x be object;
  assume
A3: x in {a} \/ ]. -infty,a.[;
  then reconsider x as Real;
  x in {a} or x in ]. -infty,a.[ by A3,XBOOLE_0:def 3;
  then x = a or x < a by TARSKI:def 1,XXREAL_1:233;
  hence thesis by XXREAL_1:234;
end;

registration
  let a be Real;
  cluster ]. a,+infty .[ -> non empty;
  coherence
  proof
    a < a + 1 by XREAL_1:29;
    hence thesis by XXREAL_1:235;
  end;
  cluster ]. -infty,a .] -> non empty;
  coherence by XXREAL_1:234;
  cluster ]. -infty,a .[ -> non empty;
  coherence
  proof
    a - 1 < a by XREAL_1:146;
    hence thesis by XXREAL_1:233;
  end;
  cluster [. a,+infty .[ -> non empty;
  coherence by XXREAL_1:236;
end;

theorem Th44:
  for a being Real holds ]. a,+infty .[ <> REAL
             by XREAL_0:def 1,XXREAL_1:235;

theorem
  for a being Real holds [. a,+infty .[ <> REAL
proof
  let a be Real;
A1: a - 1 < a by XREAL_1:146;
  a - 1 in REAL by XREAL_0:def 1;
  hence thesis by A1,XXREAL_1:236;
end;

theorem
  for a being Real holds ]. -infty, a .] <> REAL
proof
  let a be Real;
A1: a + 1 > a by XREAL_1:29;
  a + 1 in REAL by XREAL_0:def 1;
  hence thesis by A1,XXREAL_1:234;
end;

theorem Th47:
  for a being Real holds ]. -infty, a .[ <> REAL
            by XREAL_0:def 1,XXREAL_1:233;

theorem Th48:
  for A being Subset of R^1, a being Real st A = ]. a,
  +infty .[ holds Cl A = [. a,+infty .[
proof
  let A be Subset of R^1, a be Real;
  reconsider A9 = A as Subset of R^1;
  reconsider C = [. a,+infty .[ as Subset of R^1 by TOPMETR:17;
  assume
A1: A = ]. a,+infty .[;
  then
A2: A9 is open by Th39;
  C is closed by Th41;
  then
A3: Cl A9 c= C by A1,TOPS_1:5,XXREAL_1:45;
A4: C = A9 \/ {a} by A1,Th42;
  per cases by A4,A3,PRE_TOPC:18,ZFMISC_1:138;
  suppose
    Cl A9 = C;
    hence thesis;
  end;
  suppose
    Cl A9 = A9;
    hence thesis by A1,A2,Th33,Th44;
  end;
end;

theorem
  for a being Real holds Cl ]. a,+infty .[ = [. a,+infty .[
proof
  let a be Real;
  reconsider A = ]. a,+infty .[ as Subset of R^1 by TOPMETR:17;
  Cl A = [. a,+infty .[ by Th48;
  hence thesis by JORDAN5A:24;
end;

theorem Th50:
  for A being Subset of R^1, a being Real st A = ]. -infty,
  a .[ holds Cl A = ]. -infty, a .]
proof
  let A be Subset of R^1, a be Real;
  reconsider A9 = A as Subset of R^1;
  reconsider C = ]. -infty, a .] as Subset of R^1 by TOPMETR:17;
  assume
A1: A = ]. -infty, a .[;
  then
A2: A9 is open by Th39;
  C is closed by Th40;
  then
A3: Cl A9 c= C by A1,TOPS_1:5,XXREAL_1:41;
A4: C = A9 \/ {a} by A1,Th43;
  per cases by A4,A3,PRE_TOPC:18,ZFMISC_1:138;
  suppose
    Cl A9 = C;
    hence thesis;
  end;
  suppose
    Cl A9 = A9;
    hence thesis by A1,A2,Th33,Th47;
  end;
end;

theorem
  for a being Real holds Cl ]. -infty, a .[ = ]. -infty, a .]
proof
  let a be Real;
  reconsider A = ]. -infty, a .[ as Subset of R^1 by TOPMETR:17;
  Cl A = ]. -infty, a .] by Th50;
  hence thesis by JORDAN5A:24;
end;

theorem Th52:
  for A, B being Subset of R^1, b being Real st A = ].
  -infty, b .[ & B = ]. b,+infty .[ holds A, B are_separated
proof
  let A, B be Subset of R^1, b be Real;
  assume that
A1: A = ]. -infty, b .[ and
A2: B = ]. b,+infty .[;
  Cl B = [. b,+infty .[ by A2,Th48;
  then
A3: Cl B misses A by A1,XXREAL_1:94;
  Cl A = ]. -infty, b .] by A1,Th50;
  then Cl A misses B by A2,XXREAL_1:91;
  hence thesis by A3,CONNSP_1:def 1;
end;

theorem
  for A being Subset of R^1, a, b being Real st a < b & A = [. a,
  b .[ \/ ]. b,+infty .[ holds Cl A = [. a,+infty .[
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a < b and
A2: A = [. a, b .[ \/ ]. b,+infty .[;
  reconsider B = [. a, b .[, C = ]. b,+infty .[ as Subset of R^1 by TOPMETR:17;
A3: Cl A = Cl B \/ Cl C by A2,PRE_TOPC:20;
A4: Cl C = [. b,+infty .[ by Th48;
  Cl B = [. a, b .] by A1,Th34;
  hence thesis by A1,A4,A3,Th10;
end;

theorem Th54:
  for A being Subset of R^1, a, b being Real st a < b & A =
  ]. a, b .[ \/ ]. b,+infty .[ holds Cl A = [. a,+infty .[
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a < b and
A2: A = ]. a, b .[ \/ ]. b,+infty .[;
  reconsider B = ]. a, b .[, C = ]. b,+infty .[ as Subset of R^1 by TOPMETR:17;
A3: Cl A = Cl B \/ Cl C by A2,PRE_TOPC:20;
A4: Cl C = [. b,+infty .[ by Th48;
  Cl B = [. a, b .] by A1,Th15;
  hence thesis by A1,A3,A4,Th10;
end;

theorem
  for A being Subset of R^1, a, b, c being Real st a < b & b < c
  & A = RAT (a,b) \/ ]. b, c .[ \/ ]. c,+infty .[ holds Cl A = [. a,+infty .[
proof
  let A be Subset of R^1;
  let a, b, c be Real;
  assume that
A1: a < b and
A2: b < c;
  reconsider B = RAT (a,b) as Subset of R^1 by TOPMETR:17;
  reconsider C = ]. b, c .[ \/ ]. c,+infty .[ as Subset of R^1 by TOPMETR:17;
  assume A = RAT (a,b) \/ ]. b, c .[ \/ ]. c,+infty .[;
  then A = RAT (a,b) \/ C by XBOOLE_1:4;
  then Cl A = Cl B \/ Cl C by PRE_TOPC:20;
  then Cl A = Cl B \/ [. b,+infty .[ by A2,Th54;
  then Cl A = [. a, b .] \/ [. b,+infty .[ by A1,Th30;
  hence thesis by A1,Th10;
end;

theorem Th56:
  for a, b being Real holds IRRAT (a, b) misses RAT (a, b)
proof
  let a, b be Real;
  assume IRRAT (a, b) meets RAT (a, b);
  then consider x being object such that
A1: x in IRRAT (a, b) and
A2: x in RAT (a, b) by XBOOLE_0:3;
  thus thesis by A1,A2,Th29;
end;

theorem Th57:
  for a, b being Real holds REAL \ RAT (a, b) = ]. -infty,a
  .] \/ IRRAT (a, b) \/ [.b,+infty .[
proof
  let a, b be Real;
    thus REAL \ RAT (a, b) c= ]. -infty,a.] \/ IRRAT (a, b) \/ [.b,+infty .[
    proof
      let x be object;
      assume
A1:   x in REAL \ RAT (a, b);
      then
A2:   not x in RAT (a, b) by XBOOLE_0:def 5;
      reconsider x as Real by A1;
      per cases;
      suppose
        x <= a & x < b;
        then x in ]. -infty,a.] by XXREAL_1:234;
        then x in ]. -infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 3;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        x <= a & x >= b;
        then x in ]. -infty,a.] by XXREAL_1:234;
        then x in ]. -infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 3;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
A3:     x > a & x < b;
        x in IRRAT (a, b)
        proof
          per cases;
          suppose
            x is rational;
            hence thesis by A2,A3,Th28;
          end;
          suppose
            x is irrational;
            hence thesis by A3,Th29;
          end;
        end;
        then x in ]. -infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 3;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        x > a & x >= b;
        then x in [.b,+infty .[ by XXREAL_1:236;
        hence thesis by XBOOLE_0:def 3;
      end;
    end;
    let x be object;
    assume
A4: x in ]. -infty,a.] \/ IRRAT (a, b) \/ [.b,+infty .[;
    then reconsider x as Real;
A5: x in ]. -infty,a.] \/ IRRAT (a, b) or x in [.b,+infty .[ by A4,
XBOOLE_0:def 3;
    per cases by A5,XBOOLE_0:def 3;
    suppose
      x in ]. -infty,a.];
      then x <= a by XXREAL_1:234;
      then
A6:   not x in RAT (a, b) by Th28;
      x in REAL by XREAL_0:def 1;
      hence thesis by A6,XBOOLE_0:def 5;
    end;
    suppose
A7:   x in IRRAT (a, b);
      IRRAT (a, b) misses RAT (a, b) by Th56;
      then
A8:   not x in RAT (a,b) by A7,XBOOLE_0:3;
      x in REAL by XREAL_0:def 1;
      hence thesis by A8,XBOOLE_0:def 5;
    end;
    suppose
      x in [.b,+infty .[;
      then x >= b by XXREAL_1:236;
      then
A9:   not x in RAT (a, b) by Th28;
      x in REAL by XREAL_0:def 1;
      hence thesis by A9,XBOOLE_0:def 5;
    end;
end;

theorem Th58:
  for a, b being Real st a < b holds [.a,+infty .[ \ (]. a,
  b .[ \/ ]. b,+infty .[) = {a} \/ {b}
proof
  let a, b be Real;
A1: not b in ]. a,b .[ \/ ]. b,+infty .[ by XXREAL_1:205;
  assume
A2: a < b;
  then
A3: not a in ]. a,b .[ \/ ]. b,+infty .[ by XXREAL_1:223;
  [. a,+infty .[ = [. a,b .] \/ [. b,+infty .[ by A2,Th10
    .= {a, b} \/ ]. a,b .[ \/ [. b,+infty .[ by A2,XXREAL_1:128
    .= {a, b} \/ ]. a,b .[ \/ ({b} \/ ]. b,+infty .[) by Th42
    .= {a, b} \/ ]. a,b .[ \/ {b} \/ ]. b,+infty .[ by XBOOLE_1:4
    .= {a, b} \/ {b} \/ ]. a,b .[ \/ ]. b,+infty .[ by XBOOLE_1:4
    .= {a, b} \/ ]. a,b .[ \/ ]. b,+infty .[ by ZFMISC_1:9
    .= {a, b} \/ (]. a,b .[ \/ ]. b,+infty .[) by XBOOLE_1:4;
  then [.a,+infty .[ \ (]. a, b .[ \/ ]. b,+infty .[) = {a, b} by A3,A1,
XBOOLE_1:88,ZFMISC_1:51;
  hence thesis by ENUMSET1:1;
end;

theorem
  for A being Subset of R^1 st A = RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,
  +infty .[ holds A` = ]. -infty,2 .] \/ IRRAT(2,4) \/ {4} \/ {5}
proof
A1: ]. -infty,2.] \/ IRRAT (2, 4) c= ]. -infty,4.]
  proof
    let x be object;
    assume
A2: x in ]. -infty,2.] \/ IRRAT (2, 4);
    then reconsider x as Real;
    per cases by A2,XBOOLE_0:def 3;
    suppose
      x in ]. -infty,2.];
      then x <= 2 by XXREAL_1:234;
      then x <= 4 by XXREAL_0:2;
      hence thesis by XXREAL_1:234;
    end;
    suppose
      x in IRRAT (2, 4);
      then x < 4 by Th29;
      hence thesis by XXREAL_1:234;
    end;
  end;
  let A be Subset of R^1;
A3: ]. 4, 5 .[ \/ ]. 5,+infty .[ c= ]. 4,+infty .[
  proof
    let x be object;
    assume
A4: x in ]. 4, 5 .[ \/ ]. 5,+infty .[;
    then reconsider x as Real;
    per cases by A4,XBOOLE_0:def 3;
    suppose
      x in ]. 4, 5 .[;
      then x > 4 by XXREAL_1:4;
      hence thesis by XXREAL_1:235;
    end;
    suppose
      x in ]. 5,+infty .[;
      then x > 5 by XXREAL_1:235;
      then x > 4 by XXREAL_0:2;
      hence thesis by XXREAL_1:235;
    end;
  end;
  assume A = RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[;
  then
A5: A` = REAL \ (RAT (2,4) \/ (]. 4, 5 .[ \/ ]. 5,+infty .[)) by TOPMETR:17
,XBOOLE_1:4
    .= REAL \ RAT (2,4) \ (]. 4, 5 .[ \/ ]. 5,+infty .[) by XBOOLE_1:41
    .= (]. -infty,2.] \/ IRRAT (2, 4) \/ [.4,+infty .[) \ (]. 4, 5 .[ \/ ].
  5,+infty .[) by Th57;
  ]. -infty,4.] misses ]. 4,+infty .[ by XXREAL_1:91;
  then
  A` = ([.4,+infty .[ \ (]. 4, 5 .[ \/ ]. 5,+infty .[)) \/ (]. -infty,2.]
  \/ IRRAT (2, 4)) by A5,A1,A3,XBOOLE_1:64,87
    .= (]. -infty,2.] \/ IRRAT (2, 4)) \/ ({4} \/ {5}) by Th58
    .= ]. -infty,2 .] \/ IRRAT(2,4) \/ {4} \/ {5} by XBOOLE_1:4;
  hence thesis;
end;

theorem
  for A being Subset of R^1, a being Real st A = {a} holds A` =
  ]. -infty, a .[ \/ ]. a,+infty .[ by TOPMETR:17,XXREAL_1:389;

Lm7: IRRAT(2,4) \/ {4} \/ {5} c= ]. 1,+infty .[
proof
  let x be object;
  assume
A1: x in IRRAT(2,4) \/ {4} \/ {5};
  then reconsider x as Real;
A2: x in IRRAT(2,4) \/ {4} or x in {5} by A1,XBOOLE_0:def 3;
  per cases by A2,XBOOLE_0:def 3;
  suppose
    x in IRRAT(2,4);
    then x > 2 by Th29;
    then x > 1 by XXREAL_0:2;
    hence thesis by XXREAL_1:235;
  end;
  suppose
    x in {4};
    then x = 4 by TARSKI:def 1;
    hence thesis by XXREAL_1:235;
  end;
  suppose
    x in {5};
    then x = 5 by TARSKI:def 1;
    hence thesis by XXREAL_1:235;
  end;
end;

Lm8: ]. 1,+infty .[ c= [. 1,+infty .[ by XXREAL_1:45;

Lm9: ]. -infty, 1 .[ /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}) = ].
-infty, 1 .[
proof
A1: ]. -infty, 1 .[ c= ]. -infty, 2 .]
  proof
    let x be object;
    assume
A2: x in ]. -infty, 1 .[;
    then reconsider x as Real;
    x < 1 by A2,XXREAL_1:233;
    then x < 2 by XXREAL_0:2;
    hence thesis by XXREAL_1:234;
  end;
  [. 1,+infty .[ misses ]. -infty, 1 .[ by XXREAL_1:94;
  then
A3: IRRAT(2,4) \/ {4} \/ {5} misses ]. -infty, 1 .[ by Lm7,Lm8,XBOOLE_1:1,63;
  ]. -infty, 1 .[ /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}) = ].
-infty, 1 .[ /\ (]. -infty, 2 .] \/ (IRRAT(2,4) \/ {4} \/ {5})) by XBOOLE_1:113
    .= ]. -infty, 1 .[ /\ ]. -infty, 2 .] by A3,XBOOLE_1:78
    .= ]. -infty, 1 .[ by A1,XBOOLE_1:28;
  hence thesis;
end;

Lm10: ]. 1,+infty .[ /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}) = ]. 1,
2 .] \/ IRRAT(2,4) \/ {4} \/ {5}
proof
  ]. 1,+infty .[ /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}) = ]. 1,
  +infty .[ /\ (]. -infty, 2 .] \/ (IRRAT(2,4) \/ {4} \/ {5})) by XBOOLE_1:113
    .= (]. 1,+infty .[ /\ ]. -infty, 2 .]) \/ (]. 1,+infty .[ /\ (IRRAT(2,4)
  \/ {4} \/ {5})) by XBOOLE_1:23
    .= (]. 1,+infty .[ /\ ]. -infty, 2 .]) \/ (IRRAT(2,4) \/ {4} \/ {5}) by Lm7
,XBOOLE_1:28
    .= ]. 1,2 .] \/ (IRRAT(2,4) \/ {4} \/ {5}) by XXREAL_1:270
    .= ]. 1,2 .] \/ IRRAT(2,4) \/ {4} \/ {5} by XBOOLE_1:113;
  hence thesis;
end;

theorem
  (]. -infty, 1 .[ \/ ]. 1,+infty .[) /\ (]. -infty, 2 .] \/ IRRAT(2,4)
  \/ {4} \/ {5}) = ]. -infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}
proof
  (]. -infty, 1 .[ \/ ]. 1,+infty .[) /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/
{4} \/ {5}) = ]. -infty, 1 .[ \/ (]. 1,+infty .[ /\ (]. -infty, 2 .] \/ IRRAT(2
  ,4) \/ {4} \/ {5})) by Lm9,XBOOLE_1:23
    .= ]. -infty, 1 .[ \/ (]. 1, 2 .] \/ IRRAT(2,4) \/ ({4} \/ {5})) by Lm10,
XBOOLE_1:4
    .= ]. -infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,4) \/ ({4} \/ {5}) by
XBOOLE_1:113;
  hence thesis by XBOOLE_1:4;
end;

theorem
  for A being Subset of R^1, a, b being Real st a <= b & A = {a}
  \/ [. b,+infty .[ holds A` = ]. -infty, a .[ \/ ]. a, b .[
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a <= b and
A2: A = {a} \/ [. b,+infty .[;
  A` = (REAL \ [. b,+infty .[) \ {a} by A2,TOPMETR:17,XBOOLE_1:41
    .= ]. -infty,b.[ \ {a} by XXREAL_1:224,294;
  hence thesis by A1,XXREAL_1:349;
end;

theorem
  for A being Subset of R^1, a, b being Real st a < b & A = ].
  -infty, a .[ \/ ]. a, b .[ holds Cl A = ]. -infty, b .]
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a < b and
A2: A = ]. -infty, a .[ \/ ]. a, b .[;
  reconsider B = ]. -infty, a .[, C = ]. a, b .[ as Subset of R^1 by TOPMETR:17
;
A3: Cl C = [. a, b .] by A1,Th15;
  Cl A = Cl B \/ Cl C by A2,PRE_TOPC:20
    .= ]. -infty, a .] \/ [. a, b .] by A3,Th50
    .= ]. -infty, b .] by A1,Th11;
  hence thesis;
end;

theorem Th64:
  for A being Subset of R^1, a, b being Real st a < b & A =
  ]. -infty, a .[ \/ ]. a, b .] holds Cl A = ]. -infty, b .]
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a < b and
A2: A = ]. -infty, a .[ \/ ]. a, b .];
  reconsider B = ]. -infty, a .[, C = ]. a, b .] as Subset of R^1 by TOPMETR:17
;
A3: Cl C = [. a, b .] by A1,Th35;
  Cl A = Cl B \/ Cl C by A2,PRE_TOPC:20
    .= ]. -infty, a .] \/ [. a, b .] by A3,Th50
    .= ]. -infty, b .] by A1,Th11;
  hence thesis;
end;

theorem Th65:
  for A being Subset of R^1, a, b, c being Real st a < b &
b < c & A = ]. -infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c} holds Cl A = ].
  -infty, c .]
proof
  let A be Subset of R^1, a, b, c be Real;
  assume that
A1: a < b and
A2: b < c and
A3: A = ]. -infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c};
  reconsider B = ]. -infty, a .[, C = ]. a, b .], D = IRRAT(b,c), E = {c} as
  Subset of R^1 by TOPMETR:17;
A4: c in ]. -infty, c .] by XXREAL_1:234;
  Cl A = Cl (B \/ C \/ D) \/ Cl E by A3,PRE_TOPC:20
    .= Cl (B \/ C \/ D) \/ E by Th37
    .= Cl (B \/ C) \/ Cl D \/ E by PRE_TOPC:20
    .= ]. -infty, b .] \/ Cl D \/ E by A1,Th64
    .= ]. -infty, b .] \/ [. b,c .] \/ E by A2,Th31
    .= ]. -infty, c .] \/ E by A2,Th11
    .= ]. -infty, c .] by A4,ZFMISC_1:40;
  hence thesis;
end;

theorem
  for A being Subset of R^1, a, b, c, d being Real st a < b & b <
c & A = ]. -infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c} \/ {d} holds Cl A =
  ]. -infty, c .] \/ {d}
proof
  let A be Subset of R^1, a, b, c, d be Real;
  assume that
A1: a < b and
A2: b < c and
A3: A = ]. -infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c} \/ {d};
  reconsider B = ]. -infty, a .[, C = ]. a, b .], D = IRRAT(b,c), E = {c}, F =
  {d} as Subset of R^1 by TOPMETR:17;
  Cl A = Cl (B \/ C \/ D \/ E) \/ Cl F by A3,PRE_TOPC:20
    .= Cl (B \/ C \/ D \/ E) \/ {d} by Th37;
  hence thesis by A1,A2,Th65;
end;

theorem
  for A being Subset of R^1, a, b being Real st a <= b & A = ].
  -infty, a .] \/ {b} holds A` = ]. a, b .[ \/ ]. b,+infty .[
proof
  let A be Subset of R^1, a, b be Real;
  assume that
A1: a <= b and
A2: A = ]. -infty, a .] \/ {b};
  A` = (REAL \ ]. -infty, a .]) \ {b} by A2,TOPMETR:17,XBOOLE_1:41
    .= ]. a,+infty .[ \ {b} by XXREAL_1:224,288
    .= ]. a, b .[ \/ ]. b,+infty .[ by A1,XXREAL_1:365;
  hence thesis;
end;

theorem
  for a, b being Real holds [. a,+infty .[ \/ {b} <> REAL
proof
  let a, b be Real;
  set ab = min (a,b) - 1;
A1: ab < min (a,b) by XREAL_1:146;
  min (a,b) <= b by XXREAL_0:17;
  then
A2: not ab in {b} by A1,TARSKI:def 1;
  min (a,b) <= a by XXREAL_0:17;
  then ab < a by XREAL_1:146,XXREAL_0:2;
  then
A3: not ab in [. a,+infty .[ by XXREAL_1:236;
  ab in REAL by XREAL_0:def 1;
  hence thesis by A3,A2,XBOOLE_0:def 3;
end;

theorem
  for a, b being Real holds ]. -infty, a .] \/ {b} <> REAL
proof
  let a, b be Real;
  set ab = max (a,b) + 1;
A1: ab > max (a,b) by XREAL_1:29;
  max (a,b) >= a by XXREAL_0:25;
  then ab > a by A1,XXREAL_0:2;
  then
A2: not ab in ]. -infty, a.] by XXREAL_1:234;
  max (a,b) >= b by XXREAL_0:25;
  then
A3: not ab in {b} by A1,TARSKI:def 1;
  ab in REAL by XREAL_0:def 1;
  hence thesis by A2,A3,XBOOLE_0:def 3;
end;

theorem
  for TS being TopStruct, A, B being Subset of TS st A <> B holds A` <> B`
proof
  let TS be TopStruct, A, B be Subset of TS;
  assume
A1: A <> B;
  assume A` = B`;
  then A = B``;
  hence thesis by A1;
end;

theorem
  for A being Subset of R^1 st REAL = A` holds A = {}
proof
  reconsider AB = {}R^1 as Subset of R^1;
  let A be Subset of R^1;
  assume REAL = A`;
  then AB` = A` by TOPMETR:17;
  then AB = A``;
  hence thesis;
end;

begin :: Subcontinua of a real line

theorem Th72:
  for X being compact Subset of R^1, X9 being Subset of REAL st
  X9 = X holds X9 is bounded_above bounded_below
proof
  let X be compact Subset of R^1, X9 be Subset of REAL;
  assume X9 = X;
  then X9 is compact by JORDAN5A:25;
  then X9 is real-bounded by RCOMP_1:10;
  hence thesis by XXREAL_2:def 11;
end;

theorem Th73:
  for X being compact Subset of R^1, X9 being Subset of REAL, x
  being Real st x in X9 & X9 = X holds lower_bound X9 <= x &
   x <= upper_bound X9
proof
  let X be compact Subset of R^1, X9 be Subset of REAL, x be Real;
  assume that
A1: x in X9 and
A2: X9 = X;
  X9 is bounded_above bounded_below by A2,Th72;
  hence thesis by A1,SEQ_4:def 1,def 2;
end;

theorem Th74:
  for C being non empty compact connected Subset of R^1, C9 being
  Subset of REAL st C = C9 & [. lower_bound C9, upper_bound C9 .] c= C9
   holds [. lower_bound C9, upper_bound C9.] = C9
proof
  let C be non empty compact connected Subset of R^1, C9 be Subset of REAL;
  assume that
A1: C = C9 and
A2: [. lower_bound C9, upper_bound C9 .] c= C9;
  assume [. lower_bound C9, upper_bound C9 .] <> C9;
  then not C9 c= [. lower_bound C9, upper_bound C9 .] by A2,XBOOLE_0:def 10;
  then consider c being object such that
A3: c in C9 and
A4: not c in [. lower_bound C9, upper_bound C9 .];
  reconsider c as Real by A3;
A5: c <= upper_bound C9 by A1,A3,Th73;
  lower_bound C9 <= c by A1,A3,Th73;
  hence thesis by A4,A5,XXREAL_1:1;
end;

theorem Th75:
  for A being connected Subset of R^1, a, b, c being Real
  st a <= b & b <= c & a in A & c in A holds b in A
proof
  let A be connected Subset of R^1, a, b, c be Real;
  assume that
A1: a <= b and
A2: b <= c and
A3: a in A and
A4: c in A;
  per cases by A1,A2,A3,A4,XXREAL_0:1;
  suppose
    a = b or b = c;
    hence thesis by A3,A4;
  end;
  suppose
A5: a < b & b < c & a in A & c in A;
    reconsider B = ]. -infty,b .[, C = ]. b,+infty .[ as Subset of R^1 by
TOPMETR:17;
    assume not b in A;
    then A c= REAL \ {b} by TOPMETR:17,ZFMISC_1:34;
    then
A6: A c= ]. -infty,b .[ \/ ]. b,+infty .[ by XXREAL_1:389;
    now
      per cases by A6,Th52,CONNSP_1:16;
      suppose
        A c= B;
        hence contradiction by A5,XXREAL_1:233;
      end;
      suppose
        A c= C;
        hence contradiction by A5,XXREAL_1:235;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th76:
  for A being connected Subset of R^1, a, b being Real st
  a in A & b in A holds [.a,b.] c= A
proof
  let A be connected Subset of R^1, a, b be Real;
  assume that
A1: a in A and
A2: b in A;
  let x be object;
  assume x in [.a,b.];
  then x in { y where y is Real: a <= y & y <= b } by RCOMP_1:def 1;
  then ex z being Real st z = x & a <= z & z <= b;
  hence thesis by A1,A2,Th75;
end;

theorem Th77:
  for X being non empty compact connected Subset of R^1 holds X
  is non empty non empty closed_interval Subset of REAL
proof
  let C be non empty compact connected Subset of R^1;
  reconsider C9 = C as non empty Subset of REAL by TOPMETR:17;
  C is closed by COMPTS_1:7;
  then
A1: C9 is closed by JORDAN5A:23;
  then
A2: upper_bound C9 in C9 by Th72,RCOMP_1:12;
  C9 is bounded_below bounded_above by Th72;
  then C9 is real-bounded by XXREAL_2:def 11;
  then
A3: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
  lower_bound C9 in C9 by A1,Th72,RCOMP_1:13;
  then [. lower_bound C9, upper_bound C9 .] = C9 by A2,Th74,Th76;
  then C9 is non empty closed_interval by A3,MEASURE5:14;
  hence thesis;
end;

theorem
  for A being non empty compact connected Subset of R^1 holds ex a, b
  being Real st a <= b & A = [. a, b .]
proof
  let C be non empty compact connected Subset of R^1;
  reconsider C9 = C as non empty closed_interval Subset of REAL by Th77;
A1: lower_bound C9 <= upper_bound C9 by BORSUK_4:28;
A2: C9 = [. lower_bound C9, upper_bound C9 .] by INTEGRA1:4;
  then
A3: upper_bound C9 in C by A1,XXREAL_1:1;
  lower_bound C9 in C by A2,A1,XXREAL_1:1;
  then reconsider p1 = lower_bound C9, p2 = upper_bound C9 as Point of R^1
   by A3;
  take p1, p2;
  thus p1 <= p2 by BORSUK_4:28;
  thus thesis by INTEGRA1:4;
end;

registration
  let T be TopSpace;
  cluster open closed non empty for Subset-Family of T;
  existence
  proof
    reconsider F = {{}T} as Subset-Family of T by ZFMISC_1:31;
A1: F is closed
    by TARSKI:def 1;
    F is open
    by TARSKI:def 1;
    hence thesis by A1;
  end;
end;