YELLOW12

:: On the Characterization of {H}ausdorff Spaces
::  by Artur Korni{\l}owicz
::
:: Received April 18, 1998
:: Copyright (c) 1998-2026 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 XBOOLE_0, TARSKI, RELAT_1, PARTFUN1, MCART_1, ZFMISC_1, FUNCT_1,
      FUNCT_3, SUBSET_1, WAYBEL_0, ORDERS_2, LATTICES, LATTICE3, YELLOW_0,
      ORDINAL2, EQREL_1, RELAT_2, WAYBEL_3, WAYBEL_2, STRUCT_0, WELLORD1,
      WAYBEL11, XXREAL_0, REWRITE1, SETFAM_1, PRE_TOPC, RLVECT_3, CANTOR_1,
      RCOMP_1, CONNSP_2, TOPS_1, TOPS_2, T_0TOPSP, COMPTS_1, YELLOW_9, FUNCT_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, MCART_1, FUNCT_3, DOMAIN_1,
      STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CANTOR_1, CONNSP_2,
      BORSUK_1, BORSUK_2, T_0TOPSP, WELLORD1, ORDERS_2, LATTICE3, YELLOW_0,
      WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_8, WAYBEL11,
      YELLOW_9;
 constructors SETFAM_1, TOLER_1, TOPS_1, TOPS_2, T_0TOPSP, CANTOR_1, BORSUK_2,
      ORDERS_3, YELLOW_4, WAYBEL_3, YELLOW_8, WAYBEL11, YELLOW_9, CONNSP_2,
      DOMAIN_1, COMPTS_1, WAYBEL_2;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, BORSUK_1, LATTICE3,
      YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_9,
      PRE_TOPC, TOPS_1, BORSUK_2, FUNCT_2;
 requirements SUBSET, BOOLE;
 definitions TARSKI, FUNCT_1, PRE_TOPC, TOPS_2, BORSUK_1, T_0TOPSP, LATTICE3,
      YELLOW_0, WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL11, XBOOLE_0;
 equalities LATTICE3, WAYBEL_3, SUBSET_1, BINOP_1, STRUCT_0;
 expansions TARSKI, FUNCT_1, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0;
 theorems FUNCT_1, FUNCT_2, FUNCT_3, RELAT_1, TOPS_1, TOPS_2, TOPS_3, PRE_TOPC,
      CONNSP_2, BORSUK_1, ZFMISC_1, TARSKI, ORDERS_2, YELLOW_0, YELLOW_2,
      YELLOW_3, YELLOW_4, WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_7, YELLOW_8,
      YELLOW_9, WAYBEL_8, WAYBEL_3, TEX_2, SETFAM_1, CANTOR_1, XBOOLE_0,
      XBOOLE_1, EQREL_1, XTUPLE_0;

begin  :: The properties of some functions

reserve A, B, X, Y for set;

registration
  let X be empty set;
  cluster union X -> empty;
  coherence by ZFMISC_1:2;
end;

Lm1: now
  let S, T, x1, x2 be set such that
A1: x1 in S & x2 in T;
A2: dom <:pr2(S,T),pr1(S,T):> = dom pr2(S,T) /\ dom pr1(S,T) by FUNCT_3:def 7
    .= dom pr2(S,T) /\ [:S,T:] by FUNCT_3:def 4
    .= [:S,T:] /\ [:S,T:] by FUNCT_3:def 5
    .= [:S,T:];
  [x1,x2] in [:S,T:] by A1,ZFMISC_1:87;
  hence <:pr2(S,T),pr1(S,T):>.(x1,x2) = [pr2(S,T).(x1,x2),pr1(S,T).(x1,x2)] by
A2,FUNCT_3:def 7
    .= [x2,pr1(S,T).(x1,x2)] by A1,FUNCT_3:def 5
    .= [x2,x1] by A1,FUNCT_3:def 4;
end;

theorem
  (delta X).:A c= [:A,A:]
proof
  set f = delta X;
  let y be object;
  assume y in f.:A;
  then consider x being object such that
A1: x in dom f and
A2: x in A and
A3: y = f.x by FUNCT_1:def 6;
  y = [x,x] by A1,A3,FUNCT_3:def 6;
  hence thesis by A2,ZFMISC_1:def 2;
end;

theorem Th2:
  (delta X)"[:A,A:] c= A
proof
  set f = delta X;
  let x be object;
  assume x in f"[:A,A:];
  then f.x in [:A,A:] & f.x = [x,x] by FUNCT_1:def 7,FUNCT_3:def 6;
  hence thesis by ZFMISC_1:87;
end;

theorem
  for A being Subset of X holds (delta X)"[:A,A:] = A
proof
  let A be Subset of X;
  set f = delta X;
  thus f"[:A,A:] c= A by Th2;
  let x be object;
  assume
A1: x in A;
  then f.x = [x,x] by FUNCT_3:def 6;
  then dom f = X & f.x in [:A,A:] by A1,FUNCT_3:def 6,ZFMISC_1:87;
  hence thesis by A1,FUNCT_1:def 7;
end;

theorem Th4:
  dom <:pr2(X,Y),pr1(X,Y):> = [:X,Y:] & rng <:pr2(X,Y),pr1(X,Y):> = [:Y,X:]
proof
  set f = <:pr2(X,Y),pr1(X,Y):>;
  thus
A1: dom f = dom pr2(X,Y) /\ dom pr1(X,Y) by FUNCT_3:def 7
    .= dom pr2(X,Y) /\ [:X,Y:] by FUNCT_3:def 4
    .= [:X,Y:] /\ [:X,Y:] by FUNCT_3:def 5
    .= [:X,Y:];
  rng f c= [:rng pr2(X,Y),rng pr1(X,Y):] by FUNCT_3:51;
  hence rng f c= [:Y,X:] by XBOOLE_1:1;
  let y be object;
  assume y in [:Y,X:];
  then consider y1, y2 being object such that
A2: y1 in Y & y2 in X and
A3: y = [y1,y2] by ZFMISC_1:def 2;
A4: [y2,y1] in dom f by A1,A2,ZFMISC_1:87;
  f.(y2,y1) = y by A2,A3,Lm1;
  hence thesis by A4,FUNCT_1:def 3;
end;

theorem Th5:
  <:pr2(X,Y),pr1(X,Y):>.:[:A,B:] c= [:B,A:]
proof
  set f = <:pr2(X,Y),pr1(X,Y):>;
  let y be object;
  assume y in f.:[:A,B:];
  then consider x being object such that
A1: x in dom f and
A2: x in [:A,B:] and
A3: y = f.x by FUNCT_1:def 6;
  consider x1, x2 being object such that
A4: x1 in A & x2 in B and
A5: x = [x1,x2] by A2,ZFMISC_1:def 2;
  dom f = [:X,Y:] by Th4;
  then x1 in X & x2 in Y by A1,A5,ZFMISC_1:87;
  then f.(x1,x2) = [x2,x1] by Lm1;
  hence thesis by A3,A4,A5,ZFMISC_1:87;
end;

theorem
  for A being Subset of X, B being Subset of Y holds <:pr2(X,Y),pr1(X,Y)
  :>.:[:A,B:] = [:B,A:]
proof
  let A be Subset of X, B be Subset of Y;
  set f = <:pr2(X,Y),pr1(X,Y):>;
A1: dom f = [:X,Y:] by Th4;
  thus f.:[:A,B:] c= [:B,A:] by Th5;
  let y be object;
  assume y in [:B,A:];
  then consider y1, y2 being object such that
A2: y1 in B & y2 in A and
A3: y = [y1,y2] by ZFMISC_1:def 2;
  [y2,y1] in [:A,B:] & f.(y2,y1) = [y1,y2] by A2,Lm1,ZFMISC_1:87;
  hence thesis by A1,A3,FUNCT_1:def 6;
end;

theorem Th7:
  <:pr2(X,Y),pr1(X,Y):> is one-to-one
proof
  set f = <:pr2(X,Y),pr1(X,Y):>;
  let x, y be object such that
A1: x in dom f and
A2: y in dom f and
A3: f.x = f.y;
A4: dom f = [:X,Y:] by Th4;
  then consider x1, x2 being object such that
A5: x1 in X & x2 in Y and
A6: x = [x1,x2] by A1,ZFMISC_1:def 2;
  consider y1, y2 being object such that
A7: y1 in X & y2 in Y and
A8: y = [y1,y2] by A4,A2,ZFMISC_1:def 2;
A9: f.(y1,y2) = [y2,y1] by A7,Lm1;
A10: f.(x1,x2) = [x2,x1] by A5,Lm1;
  then x1 = y1 by A3,A6,A8,A9,XTUPLE_0:1;
  hence thesis by A3,A6,A8,A10,A9,XTUPLE_0:1;
end;

registration
  let X, Y be set;
  cluster <:pr2(X,Y),pr1(X,Y):> -> one-to-one;
  coherence by Th7;
end;

theorem Th8:
  <:pr2(X,Y),pr1(X,Y):>" = <:pr2(Y,X),pr1(Y,X):>
proof
  set f = <:pr2(X,Y),pr1(X,Y):>, g = <:pr2(Y,X),pr1(Y,X):>;
A1: dom (f") = rng f by FUNCT_1:32
    .= [:Y,X:] by Th4;
A2: now
    let x be object;
    assume x in [:Y,X:];
    then consider x1, x2 being object such that
A3: x1 in Y & x2 in X and
A4: x = [x1,x2] by ZFMISC_1:def 2;
A5: g.(x1,x2) = [x2,x1] & f.(x2,x1) = [x1,x2] by A3,Lm1;
    dom f = [:X,Y:] by Th4;
    then [x2,x1] in dom f by A3,ZFMISC_1:87;
    hence f".x = g.x by A4,A5,FUNCT_1:32;
  end;
  dom g = [:Y,X:] by Th4;
  hence thesis by A1,A2;
end;

begin  :: The properties of the relational structures

theorem Th9:
  for L1 being Semilattice, L2 being non empty RelStr for x, y
  being Element of L1, x1, y1 being Element of L2 st the RelStr of L1 = the
  RelStr of L2 & x = x1 & y = y1 holds x "/\" y = x1 "/\" y1
proof
  let L1 be Semilattice, L2 be non empty RelStr, x, y be Element of L1, x1, y1
  be Element of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: x = x1 & y = y1;
A3: L2 is with_infima Poset by A1,WAYBEL_8:12,13,14,YELLOW_7:14;
A4: ex_inf_of {x,y}, L1 by YELLOW_0:21;
  thus x "/\" y = inf{x,y} by YELLOW_0:40
    .= inf{x1,y1} by A1,A2,A4,YELLOW_0:27
    .= x1 "/\" y1 by A3,YELLOW_0:40;
end;

theorem Th10:
  for L1 being sup-Semilattice, L2 being non empty RelStr for x, y
  being Element of L1, x1, y1 being Element of L2 st the RelStr of L1 = the
  RelStr of L2 & x = x1 & y = y1 holds x "\/" y = x1 "\/" y1
proof
  let L1 be sup-Semilattice, L2 be non empty RelStr, x, y be Element of L1, x1
  , y1 be Element of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: x = x1 & y = y1;
A3: L2 is with_suprema Poset by A1,WAYBEL_8:12,13,14,YELLOW_7:15;
A4: ex_sup_of {x,y}, L1 by YELLOW_0:20;
  thus x "\/" y = sup{x,y} by YELLOW_0:41
    .= sup{x1,y1} by A1,A2,A4,YELLOW_0:26
    .= x1 "\/" y1 by A3,YELLOW_0:41;
end;

theorem Th11:
  for L1 being Semilattice, L2 being non empty RelStr for X, Y
being Subset of L1, X1, Y1 being Subset of L2 st the RelStr of L1 = the RelStr
  of L2 & X = X1 & Y = Y1 holds X "/\" Y = X1 "/\" Y1
proof
  let L1 be Semilattice, L2 be non empty RelStr, X, Y be Subset of L1, X1, Y1
  be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: X = X1 & Y = Y1;
  set XY = { x "/\" y where x, y is Element of L1 : x in X & y in Y }, XY1 = {
  x "/\" y where x, y is Element of L2 : x in X1 & y in Y1 };
A3: XY = XY1
  proof
    hereby
      let a be object;
      assume a in XY;
      then consider x, y being Element of L1 such that
A4:   a = x "/\" y and
A5:   x in X & y in Y;
      reconsider x1 = x, y1 = y as Element of L2 by A1;
      a = x1 "/\" y1 by A1,A4,Th9;
      hence a in XY1 by A2,A5;
    end;
    let a be object;
    assume a in XY1;
    then consider x, y being Element of L2 such that
A6: a = x "/\" y and
A7: x in X1 & y in Y1;
    reconsider x1 = x, y1 = y as Element of L1 by A1;
    a = x1 "/\" y1 by A1,A6,Th9;
    hence thesis by A2,A7;
  end;
  thus X "/\" Y = XY by YELLOW_4:def 4
    .= X1 "/\" Y1 by A3,YELLOW_4:def 4;
end;

theorem
  for L1 being sup-Semilattice, L2 being non empty RelStr for X, Y being
Subset of L1, X1, Y1 being Subset of L2 st the RelStr of L1 = the RelStr of L2
  & X = X1 & Y = Y1 holds X "\/" Y = X1 "\/" Y1
proof
  let L1 be sup-Semilattice, L2 be non empty RelStr, X, Y be Subset of L1, X1,
  Y1 be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: X = X1 & Y = Y1;
  set XY = { x "\/" y where x, y is Element of L1 : x in X & y in Y }, XY1 = {
  x "\/" y where x, y is Element of L2 : x in X1 & y in Y1 };
A3: XY = XY1
  proof
    hereby
      let a be object;
      assume a in XY;
      then consider x, y being Element of L1 such that
A4:   a = x "\/" y and
A5:   x in X & y in Y;
      reconsider x1 = x, y1 = y as Element of L2 by A1;
      a = x1 "\/" y1 by A1,A4,Th10;
      hence a in XY1 by A2,A5;
    end;
    let a be object;
    assume a in XY1;
    then consider x, y being Element of L2 such that
A6: a = x "\/" y and
A7: x in X1 & y in Y1;
    reconsider x1 = x, y1 = y as Element of L1 by A1;
    a = x1 "\/" y1 by A1,A6,Th10;
    hence thesis by A2,A7;
  end;
  thus X "\/" Y = XY by YELLOW_4:def 3
    .= X1 "\/" Y1 by A3,YELLOW_4:def 3;
end;

theorem Th13:
  for L1 being antisymmetric up-complete non empty reflexive
  RelStr, L2 being non empty reflexive RelStr, x being Element of L1, y being
Element of L2 st the RelStr of L1 = the RelStr of L2 & x = y holds waybelow x =
  waybelow y & wayabove x = wayabove y
proof
  let L1 be antisymmetric up-complete non empty reflexive RelStr, L2 be non
  empty reflexive RelStr, x be Element of L1, y be Element of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: x = y;
  hereby
    hereby
      let a be object;
      assume a in waybelow x;
      then consider z being Element of L1 such that
A3:   a = z and
A4:   z << x;
      reconsider w = z as Element of L2 by A1;
      L2 is antisymmetric by A1,WAYBEL_8:14;
      then w << y by A1,A2,A4,WAYBEL_8:8;
      hence a in waybelow y by A3;
    end;
    let a be object;
    assume a in waybelow y;
    then consider z being Element of L2 such that
A5: a = z and
A6: z << y;
    reconsider w = z as Element of L1 by A1;
    L2 is up-complete antisymmetric by A1,WAYBEL_8:14,15;
    then w << x by A1,A2,A6,WAYBEL_8:8;
    hence a in waybelow x by A5;
  end;
  hereby
    let a be object;
    assume a in wayabove x;
    then consider z being Element of L1 such that
A7: a = z and
A8: z >> x;
    reconsider w = z as Element of L2 by A1;
    L2 is antisymmetric by A1,WAYBEL_8:14;
    then w >> y by A1,A2,A8,WAYBEL_8:8;
    hence a in wayabove y by A7;
  end;
  let a be object;
  assume a in wayabove y;
  then consider z being Element of L2 such that
A9: a = z and
A10: z >> y;
  reconsider w = z as Element of L1 by A1;
  L2 is up-complete antisymmetric by A1,WAYBEL_8:14,15;
  then w >> x by A1,A2,A10,WAYBEL_8:8;
  hence thesis by A9;
end;

theorem
  for L1 being meet-continuous Semilattice, L2 being non empty reflexive
  RelStr st the RelStr of L1 = the RelStr of L2 holds L2 is meet-continuous
proof
  let L1 be meet-continuous Semilattice, L2 be non empty reflexive RelStr;
  assume
A1: the RelStr of L1 = the RelStr of L2;
  hence L2 is up-complete by WAYBEL_8:15;
  let x be Element of L2, D be non empty directed Subset of L2;
  reconsider E = D as non empty directed Subset of L1 by A1,WAYBEL_0:3;
  reconsider y = x as Element of L1 by A1;
A2: {x} "/\" D = {y} "/\" E by A1,Th11;
  reconsider yy = {y} as non empty directed Subset of L1 by WAYBEL_0:5;
A3: ex_sup_of yy "/\" E, L1 by WAYBEL_0:75;
  ex_sup_of E, L1 by WAYBEL_0:75;
  then sup D = sup E by A1,YELLOW_0:26;
  hence x "/\" sup D = y "/\" sup E by A1,Th9
    .= sup ({y} "/\" E) by WAYBEL_2:def 6
    .= sup ({x} "/\" D) by A1,A2,A3,YELLOW_0:26;
end;

theorem
  for L1 being continuous antisymmetric non empty reflexive RelStr, L2
  being non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2 holds
  L2 is continuous
proof
  let L1 be continuous antisymmetric non empty reflexive RelStr, L2 be non
  empty reflexive RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
  hereby
    let y be Element of L2;
    reconsider x = y as Element of L1 by A1;
    waybelow x = waybelow y by A1,Th13;
    hence waybelow y is non empty directed by A1,WAYBEL_0:3;
  end;
  thus L2 is up-complete by A1,WAYBEL_8:15;
  let y be Element of L2;
  reconsider x = y as Element of L1 by A1;
A2: ex_sup_of waybelow x, L1 & x = sup waybelow x by WAYBEL_0:75,WAYBEL_3:def 5
;
  waybelow x = waybelow y by A1,Th13;
  hence thesis by A1,A2,YELLOW_0:26;
end;

theorem
  for L1, L2 being RelStr, A being Subset of L1, J being Subset of L2 st
  the RelStr of L1 = the RelStr of L2 & A = J holds subrelstr A = subrelstr J
proof
  let L1, L2 be RelStr, A be Subset of L1, J be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: A = J;
A3: the carrier of subrelstr A = A by YELLOW_0:def 15
    .= the carrier of subrelstr J by A2,YELLOW_0:def 15;
  then
  the InternalRel of subrelstr A = (the InternalRel of L2)|_2(the carrier
  of subrelstr J) by A1,YELLOW_0:def 14
    .= the InternalRel of subrelstr J by YELLOW_0:def 14;
  hence thesis by A3;
end;

theorem
  for L1, L2 being non empty RelStr, A being SubRelStr of L1, J being
SubRelStr of L2 st the RelStr of L1 = the RelStr of L2 & the RelStr of A = the
  RelStr of J & A is meet-inheriting holds J is meet-inheriting
proof
  let L1, L2 be non empty RelStr, A be SubRelStr of L1, J be SubRelStr of L2
  such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: the RelStr of A = the RelStr of J and
A3: for x, y being Element of L1 st x in the carrier of A & y in the
  carrier of A & ex_inf_of {x,y},L1 holds inf {x,y} in the carrier of A;
  let x, y be Element of L2 such that
A4: x in the carrier of J & y in the carrier of J and
A5: ex_inf_of {x,y},L2;
  reconsider x1 = x, y1 = y as Element of L1 by A1;
  inf {x1,y1} in the carrier of A by A1,A2,A3,A4,A5,YELLOW_0:14;
  hence thesis by A1,A2,A5,YELLOW_0:27;
end;

theorem
  for L1, L2 being non empty RelStr, A being SubRelStr of L1, J being
SubRelStr of L2 st the RelStr of L1 = the RelStr of L2 & the RelStr of A = the
  RelStr of J & A is join-inheriting holds J is join-inheriting
proof
  let L1, L2 be non empty RelStr, A be SubRelStr of L1, J be SubRelStr of L2
  such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: the RelStr of A = the RelStr of J and
A3: for x, y being Element of L1 st x in the carrier of A & y in the
  carrier of A & ex_sup_of {x,y},L1 holds sup {x,y} in the carrier of A;
  let x, y be Element of L2 such that
A4: x in the carrier of J & y in the carrier of J and
A5: ex_sup_of {x,y},L2;
  reconsider x1 = x, y1 = y as Element of L1 by A1;
  sup {x1,y1} in the carrier of A by A1,A2,A3,A4,A5,YELLOW_0:14;
  hence thesis by A1,A2,A5,YELLOW_0:26;
end;

theorem
  for L1 being up-complete antisymmetric non empty reflexive RelStr,
L2 being non empty reflexive RelStr, X being Subset of L1, Y being Subset of L2
  st the RelStr of L1 = the RelStr of L2 & X = Y & X is property(S) holds Y is
  property(S)
proof
  let L1 be up-complete antisymmetric non empty reflexive RelStr, L2 be non
  empty reflexive RelStr, X be Subset of L1, Y be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: X = Y and
A3: for D being non empty directed Subset of L1 st sup D in X ex y being
Element of L1 st y in D & for x being Element of L1 st x in D & x >= y holds x
  in X;
  let E be non empty directed Subset of L2 such that
A4: sup E in Y;
  reconsider D = E as non empty directed Subset of L1 by A1,WAYBEL_0:3;
  ex_sup_of D, L1 by WAYBEL_0:75;
  then sup D in X by A1,A2,A4,YELLOW_0:26;
  then consider y being Element of L1 such that
A5: y in D and
A6: for x being Element of L1 st x in D & x >= y holds x in X by A3;
  reconsider y2 = y as Element of L2 by A1;
  take y2;
  thus y2 in E by A5;
  let x2 be Element of L2;
  assume x2 in E & x2 >= y2;
  hence thesis by A1,A2,A6,YELLOW_0:1;
end;

theorem
  for L1 being up-complete antisymmetric non empty reflexive RelStr,
L2 being non empty reflexive RelStr, X being Subset of L1, Y being Subset of L2
  st the RelStr of L1 = the RelStr of L2 & X = Y & X is directly_closed holds Y
  is directly_closed
proof
  let L1 be up-complete antisymmetric non empty reflexive RelStr, L2 be non
  empty reflexive RelStr, X be Subset of L1, Y be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: X = Y and
A3: for D being non empty directed Subset of L1 st D c= X holds sup D in X;
  let E be non empty directed Subset of L2 such that
A4: E c= Y;
  reconsider D = E as non empty directed Subset of L1 by A1,WAYBEL_0:3;
  ex_sup_of D, L1 & sup D in X by A2,A3,A4,WAYBEL_0:75;
  hence thesis by A1,A2,YELLOW_0:26;
end;

theorem
  for N being antisymmetric with_infima RelStr, D, E being Subset of N
  for X being upper Subset of N st D misses X holds D "/\" E misses X
proof
  let N be antisymmetric with_infima RelStr, D, E be Subset of N, X be upper
  Subset of N such that
A1: D /\ X = {};
  assume (D "/\" E) /\ X <> {};
  then consider k being object such that
A2: k in (D "/\" E) /\ X by XBOOLE_0:def 1;
  reconsider k as Element of N by A2;
A3: D "/\" E = { d "/\" e where d, e is Element of N : d in D & e in E } & k
  in D "/\" E by A2,XBOOLE_0:def 4,YELLOW_4:def 4;
A4: k in X by A2,XBOOLE_0:def 4;
  consider d, e being Element of N such that
A5: k = d "/\" e and
A6: d in D and
  e in E by A3;
  d "/\" e <= d by YELLOW_0:23;
  then d in X by A4,A5,WAYBEL_0:def 20;
  hence thesis by A1,A6,XBOOLE_0:def 4;
end;

theorem
  for R being reflexive non empty RelStr holds id the carrier of R c= (
  the InternalRel of R) /\ the InternalRel of (R~)
proof
  let R be reflexive non empty RelStr;
  let a be object;
  assume
A1: a in id the carrier of R;
  then consider y, z being object such that
A2: a = [y,z] by RELAT_1:def 1;
  reconsider y, z as Element of R by A1,A2,ZFMISC_1:87;
  y <= z by A1,A2,RELAT_1:def 10;
  then
A3: a in the InternalRel of R by A2,ORDERS_2:def 5;
  y = z by A1,A2,RELAT_1:def 10;
  then a in the InternalRel of R~ by A2,A3,RELAT_1:def 7;
  hence thesis by A3,XBOOLE_0:def 4;
end;

theorem
  for R being antisymmetric RelStr holds (the InternalRel of R) /\ the
  InternalRel of (R~) c= id the carrier of R
proof
  let R be antisymmetric RelStr;
  let a be object;
  assume
A1: a in (the InternalRel of R) /\ the InternalRel of R~;
  then consider y, z being object such that
A2: a = [y,z] by RELAT_1:def 1;
A3: y in the carrier of R by A1,A2,ZFMISC_1:87;
  reconsider y, z as Element of R by A1,A2,ZFMISC_1:87;
  a in the InternalRel of R~ by A1,XBOOLE_0:def 4;
  then [z,y] in the InternalRel of R by A2,RELAT_1:def 7;
  then
A4: z <= y by ORDERS_2:def 5;
  a in the InternalRel of R by A1,XBOOLE_0:def 4;
  then y <= z by A2,ORDERS_2:def 5;
  then y = z by A4,ORDERS_2:2;
  hence thesis by A2,A3,RELAT_1:def 10;
end;

definition
  let L be non empty RelStr;
  let f be Function of [:L,L:], L;
  let a,b be Element of L;
  redefine func f.(a,b) -> Element of L;  :: redefines . (BINOP_1, definition)
  coherence
  proof
    f.[a,b] is Element of L;
    hence thesis;
  end;
end;

theorem Th24:
  for R being upper-bounded Semilattice, X being Subset of [:R,R:]
  st ex_inf_of (inf_op R).:X,R holds inf_op R preserves_inf_of X
proof
  let R be upper-bounded Semilattice;
  set f = inf_op R;
  let X be Subset of [:R,R:] such that
A1: ex_inf_of f.:X,R and
A2: ex_inf_of X,[:R,R:];
  thus ex_inf_of f.:X,R by A1;
A3: dom f = the carrier of [:R,R:] by FUNCT_2:def 1;
  then
A4: dom f = [:the carrier of R,the carrier of R:] by YELLOW_3:def 2;
A5: for b being Element of R st b is_<=_than f.:X holds f.inf X >= b
  proof
    let b be Element of R such that
A6: b is_<=_than f.:X;
    X is_>=_than [b,b]
    proof
      let c be Element of [:R,R:];
      assume c in X;
      then f.c in f.:X by A3,FUNCT_1:def 6;
      then
A7:   b <= f.c by A6;
      consider s, t being object such that
A8:   s in the carrier of R & t in the carrier of R and
A9:   c = [s,t] by A3,A4,ZFMISC_1:def 2;
      reconsider s, t as Element of R by A8;
A10:  f.c = f.(s,t) by A9
        .= s "/\" t by WAYBEL_2:def 4;
      s "/\" t <= t by YELLOW_0:23;
      then
A11:  b <= t by A7,A10,ORDERS_2:3;
      s "/\" t <= s by YELLOW_0:23;
      then b <= s by A7,A10,ORDERS_2:3;
      hence [b,b] <= c by A9,A11,YELLOW_3:11;
    end;
    then [b,b] <= inf X by A2,YELLOW_0:def 10;
    then f.(b,b) <= f.inf X by WAYBEL_1:def 2;
    then b "/\" b <= f.inf X by WAYBEL_2:def 4;
    hence b <= f.inf X by YELLOW_0:25;
  end;
  inf X is_<=_than X by A2,YELLOW_0:def 10;
  then f.inf X is_<=_than f.:X by YELLOW_2:13;
  hence thesis by A1,A5,YELLOW_0:def 10;
end;

registration
  let R be complete Semilattice;
  cluster inf_op R -> infs-preserving;
  coherence
  proof
    let X be Subset of [:R,R:] such that
A1: ex_inf_of X,[:R,R:];
    thus ex_inf_of (inf_op R).:X,R by YELLOW_0:17;
    then inf_op R preserves_inf_of X by Th24;
    hence thesis by A1;
  end;
end;

theorem Th25:
  for R being lower-bounded sup-Semilattice, X being Subset of [:R
  ,R:] st ex_sup_of (sup_op R).:X,R holds sup_op R preserves_sup_of X
proof
  let R be lower-bounded sup-Semilattice;
  set f = sup_op R;
  let X be Subset of [:R,R:] such that
A1: ex_sup_of f.:X,R and
A2: ex_sup_of X,[:R,R:];
  thus ex_sup_of f.:X,R by A1;
A3: dom f = the carrier of [:R,R:] by FUNCT_2:def 1;
  then
A4: dom f = [:the carrier of R,the carrier of R:] by YELLOW_3:def 2;
A5: for b being Element of R st b is_>=_than f.:X holds f.sup X <= b
  proof
    let b be Element of R such that
A6: b is_>=_than f.:X;
    X is_<=_than [b,b]
    proof
      let c be Element of [:R,R:];
      assume c in X;
      then f.c in f.:X by A3,FUNCT_1:def 6;
      then
A7:   f.c <= b by A6;
      consider s, t being object such that
A8:   s in the carrier of R & t in the carrier of R and
A9:   c = [s,t] by A3,A4,ZFMISC_1:def 2;
      reconsider s, t as Element of R by A8;
A10:  f.c = f.(s,t) by A9
        .= s "\/" t by WAYBEL_2:def 5;
      t <= s "\/" t by YELLOW_0:22;
      then
A11:  t <= b by A7,A10,ORDERS_2:3;
      s <= s "\/" t by YELLOW_0:22;
      then s <= b by A7,A10,ORDERS_2:3;
      hence c <= [b,b] by A9,A11,YELLOW_3:11;
    end;
    then sup X <= [b,b] by A2,YELLOW_0:def 9;
    then f.sup X <= f.(b,b) by WAYBEL_1:def 2;
    then b <= b & f.sup X <= b "\/" b by WAYBEL_2:def 5;
    hence thesis by YELLOW_0:24;
  end;
  X is_<=_than sup X by A2,YELLOW_0:def 9;
  then f.:X is_<=_than f.sup X by YELLOW_2:14;
  hence thesis by A1,A5,YELLOW_0:def 9;
end;

registration
  let R be complete sup-Semilattice;
  cluster sup_op R -> sups-preserving;
  coherence
  proof
    let X be Subset of [:R,R:] such that
A1: ex_sup_of X,[:R,R:];
    thus ex_sup_of (sup_op R).:X,R by YELLOW_0:17;
    then sup_op R preserves_sup_of X by Th25;
    hence thesis by A1;
  end;
end;

theorem
  for N being Semilattice, A being Subset of N st subrelstr A is
  meet-inheriting holds A is filtered
proof
  let N be Semilattice, A be Subset of N such that
A1: subrelstr A is meet-inheriting;
  let x, y be Element of N such that
A2: x in A & y in A;
  take x"/\"y;
A3: the carrier of subrelstr A = A by YELLOW_0:def 15;
  ex_inf_of {x,y},N by YELLOW_0:21;
  then inf {x,y} in the carrier of subrelstr A by A1,A2,A3;
  hence x"/\"y in A by A3,YELLOW_0:40;
  thus x"/\"y <= x & x"/\"y <= y by YELLOW_0:23;
end;

theorem
  for N being sup-Semilattice, A being Subset of N st subrelstr A is
  join-inheriting holds A is directed
proof
  let N be sup-Semilattice, A be Subset of N such that
A1: subrelstr A is join-inheriting;
  let x, y be Element of N such that
A2: x in A & y in A;
  take x"\/"y;
A3: the carrier of subrelstr A = A by YELLOW_0:def 15;
  ex_sup_of {x,y},N by YELLOW_0:20;
  then sup {x,y} in the carrier of subrelstr A by A1,A2,A3;
  hence x"\/"y in A by A3,YELLOW_0:41;
  thus x <= x"\/"y & y <= x"\/"y by YELLOW_0:22;
end;

theorem
  for N being transitive RelStr, A, J being Subset of N st A
  is_coarser_than uparrow J holds uparrow A c= uparrow J
proof
  let N be transitive RelStr, A, J be Subset of N such that
A1: A is_coarser_than uparrow J;
  let w be object;
  assume
A2: w in uparrow A;
  then reconsider w1 = w as Element of N;
  consider t being Element of N such that
A3: t <= w1 and
A4: t in A by A2,WAYBEL_0:def 16;
  consider t1 being Element of N such that
A5: t1 in uparrow J and
A6: t1 <= t by A1,A4,YELLOW_4:def 2;
  consider t2 being Element of N such that
A7: t2 <= t1 and
A8: t2 in J by A5,WAYBEL_0:def 16;
  t2 <= t by A6,A7,ORDERS_2:3;
  then t2 <= w1 by A3,ORDERS_2:3;
  hence thesis by A8,WAYBEL_0:def 16;
end;

theorem
  for N being transitive RelStr, A, J being Subset of N st A
  is_finer_than downarrow J holds downarrow A c= downarrow J
proof
  let N be transitive RelStr, A, J be Subset of N such that
A1: A is_finer_than downarrow J;
  let w be object;
  assume
A2: w in downarrow A;
  then reconsider w1 = w as Element of N;
  consider t being Element of N such that
A3: w1 <= t and
A4: t in A by A2,WAYBEL_0:def 15;
  consider t1 being Element of N such that
A5: t1 in downarrow J and
A6: t <= t1 by A1,A4,YELLOW_4:def 1;
  consider t2 being Element of N such that
A7: t1 <= t2 and
A8: t2 in J by A5,WAYBEL_0:def 15;
  w1 <= t1 by A3,A6,ORDERS_2:3;
  then w1 <= t2 by A7,ORDERS_2:3;
  hence thesis by A8,WAYBEL_0:def 15;
end;

theorem
  for N being non empty reflexive RelStr for x being Element of N, X
  being Subset of N st x in X holds uparrow x c= uparrow X
proof
  let N be non empty reflexive RelStr, x be Element of N, X be Subset of N
  such that
A1: x in X;
  let a be object;
  assume
A2: a in uparrow x;
  then reconsider b = a as Element of N;
  x <= b by A2,WAYBEL_0:18;
  hence thesis by A1,WAYBEL_0:def 16;
end;

theorem
  for N being non empty reflexive RelStr for x being Element of N, X
  being Subset of N st x in X holds downarrow x c= downarrow X
proof
  let N be non empty reflexive RelStr, x be Element of N, X be Subset of N
  such that
A1: x in X;
  let a be object;
  assume
A2: a in downarrow x;
  then reconsider b = a as Element of N;
  b <= x by A2,WAYBEL_0:17;
  hence thesis by A1,WAYBEL_0:def 15;
end;

begin  :: On the Hausdorff Spaces

reserve R, S, T for non empty TopSpace;

theorem Th32:
  for S, T being TopStruct, B being Basis of S st the TopStruct of
  S = the TopStruct of T holds B is Basis of T
proof
  let S, T be TopStruct, B be Basis of S;
A1: B c= the topology of S by TOPS_2:64;
  assume
A2: the TopStruct of S = the TopStruct of T;
  then the topology of T c= UniCl B by CANTOR_1:def 2;
  hence thesis by A2,A1,CANTOR_1:def 2,TOPS_2:64;
end;

theorem Th33:
  for S, T being TopStruct, B being prebasis of S st the TopStruct
  of S = the TopStruct of T holds B is prebasis of T
proof
  let S, T be TopStruct, B be prebasis of S;
  consider F being Basis of S such that
A1: F c= FinMeetCl B by CANTOR_1:def 4;
  assume
A2: the TopStruct of S = the TopStruct of T;
  then B c= the topology of T & F is Basis of T by Th32,TOPS_2:64;
  hence thesis by A2,A1,CANTOR_1:def 4,TOPS_2:64;
end;

theorem Th34:
  for J being Basis of T holds J is non empty
proof
  let J be Basis of T;
  assume J is empty;
  then
A1: UniCl J = {{}} by YELLOW_9:16;
  the topology of T c= UniCl J & the carrier of T in the topology of T by
CANTOR_1:def 2,PRE_TOPC:def 1;
  hence contradiction by A1,TARSKI:def 1;
end;

registration
  let T be non empty TopSpace;
  cluster -> non empty for Basis of T;
  coherence by Th34;
end;

theorem Th35:
  for x being Point of T, J being Basis of x holds J is non empty
proof
  let x be Point of T, J be Basis of x;
  ex W being Subset of T st W in J & W c= [#]T by YELLOW_8:13;
  hence thesis;
end;

registration
  let T be non empty TopSpace, x be Point of T;
  cluster -> non empty for Basis of x;
  coherence by Th35;
end;

theorem
  for S1, T1, S2, T2 being TopSpace, f being Function of S1, S2, g being
Function of T1, T2 st the TopStruct of S1 = the TopStruct of T1 & the TopStruct
  of S2 = the TopStruct of T2 & f = g & f is continuous holds g is continuous
proof
  let S1, T1, S2, T2 be TopSpace, f be Function of S1, S2, g be Function of T1
  , T2 such that
A1: the TopStruct of S1 = the TopStruct of T1 and
A2: the TopStruct of S2 = the TopStruct of T2 and
A3: f = g and
A4: f is continuous;
  now
    let P2 be Subset of T2 such that
A5: P2 is closed;
    reconsider P1 = P2 as Subset of S2 by A2;
    P1 is closed by A2,A5,TOPS_3:79;
    then f"P1 is closed by A4;
    hence g"P2 is closed by A1,A3,TOPS_3:79;
  end;
  hence thesis;
end;

theorem Th37:
  id the carrier of T = {p where p is Point of [:T,T:]: pr1(the
  carrier of T,the carrier of T).p = pr2(the carrier of T,the carrier of T).p}
proof
  set f = pr1(the carrier of T,the carrier of T), g = pr2(the carrier of T,the
  carrier of T);
A1: the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by
BORSUK_1:def 2;
  hereby
    let a be object;
    assume
A2: a in id the carrier of T;
    then consider x, y being object such that
A3: x in the carrier of T and
A4: y in the carrier of T and
A5: a = [x,y] by ZFMISC_1:def 2;
A6: x = y by A2,A5,RELAT_1:def 10;
    f.(x,y) = x by A3,A4,FUNCT_3:def 4
      .= g.(x,y) by A3,A6,FUNCT_3:def 5;
    hence a in {p where p is Point of [:T,T:]: f.p = g.p} by A1,A2,A5;
  end;
  let a be object;
  assume a in {p where p is Point of [:T,T:]: f.p = g.p};
  then consider p being Point of [:T,T:] such that
A7: a = p and
A8: f.p = g.p;
  consider x, y being object such that
A9: x in the carrier of T and
A10: y in the carrier of T and
A11: p = [x,y] by A1,ZFMISC_1:def 2;
A12: f.(x,y) = g.(x,y) by A8,A11;
  x = f.(x,y) by A9,A10,FUNCT_3:def 4
    .= y by A9,A10,A12,FUNCT_3:def 5;
  hence thesis by A7,A9,A11,RELAT_1:def 10;
end;

theorem Th38:
  delta the carrier of T is continuous Function of T, [:T,T:]
proof
  the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by
BORSUK_1:def 2;
  then reconsider f = delta the carrier of T as Function of T, [:T,T:];
  f is continuous
  proof
    let W be Point of T, G be a_neighborhood of f.W;
    consider A being Subset-Family of [:T,T:] such that
A1: Int G = union A and
A2: for e being set st e in A ex X1, Y1 being Subset of T st e = [:X1,
    Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
    f.W in Int G by CONNSP_2:def 1;
    then consider Z being set such that
A3: f.W in Z and
A4: Z in A by A1,TARSKI:def 4;
    consider X1, Y1 being Subset of T such that
A5: Z = [:X1,Y1:] and
A6: X1 is open & Y1 is open by A2,A4;
    f.W = [W,W] by FUNCT_3:def 6;
    then W in X1 & W in Y1 by A3,A5,ZFMISC_1:87;
    then
A7: W in X1 /\ Y1 by XBOOLE_0:def 4;
    X1 /\ Y1 is open by A6;
    then W in Int (X1 /\ Y1) by A7,TOPS_1:23;
    then reconsider H = X1 /\ Y1 as a_neighborhood of W by CONNSP_2:def 1;
A8: f.:H c= Int G
    proof
      let y be object;
      assume y in f.:H;
      then consider x being object such that
A9:   x in dom f and
A10:  x in H and
A11:  y = f.x by FUNCT_1:def 6;
A12:  x in X1 & x in Y1 by A10,XBOOLE_0:def 4;
      y = [x,x] by A9,A11,FUNCT_3:def 6;
      then y in Z by A5,A12,ZFMISC_1:87;
      hence thesis by A1,A4,TARSKI:def 4;
    end;
    take H;
    Int G c= G by TOPS_1:16;
    hence thesis by A8;
  end;
  hence thesis;
end;

theorem Th39:
  pr1(the carrier of S,the carrier of T) is continuous Function of [:S,T:], S
proof
  set I = the carrier of S, J = the carrier of T;
A1: the carrier of [:S,T:] = [:I,J:] by BORSUK_1:def 2;
  then reconsider f = pr1(I,J) as Function of [:S,T:], S;
  f is continuous
  proof
    let w be Point of [:S,T:], G be a_neighborhood of f.w;
    set H = [:Int G, [#]T:];
A2: Int H = [:Int Int G, Int [#]T:] by BORSUK_1:7
      .= [:Int G, [#]T:] by TOPS_1:15;
    consider x, y being object such that
A3: x in I and
A4: y in J and
A5: w = [x,y] by A1,ZFMISC_1:def 2;
    f.w in Int G & f.(x,y) = x by A3,A4,CONNSP_2:def 1,FUNCT_3:def 4;
    then w in Int H by A4,A5,A2,ZFMISC_1:def 2;
    then reconsider H as a_neighborhood of w by CONNSP_2:def 1;
    take H;
    reconsider X = Int G as non empty Subset of S by CONNSP_2:def 1;
    [:X,[#]T:] <> {};
    then f.:H = Int G by EQREL_1:49;
    hence thesis by TOPS_1:16;
  end;
  hence thesis;
end;

theorem Th40:
  pr2(the carrier of S,the carrier of T) is continuous Function of [:S,T:], T
proof
  set I = the carrier of S, J = the carrier of T;
A1: the carrier of [:S,T:] = [:I,J:] by BORSUK_1:def 2;
  then reconsider f = pr2(I,J) as Function of [:S,T:], T;
  f is continuous
  proof
    let w be Point of [:S,T:], G be a_neighborhood of f.w;
    set H = [:[#]S,Int G:];
A2: Int H = [:Int [#]S,Int Int G:] by BORSUK_1:7
      .= [:[#]S,Int G:] by TOPS_1:15;
    consider x, y being object such that
A3: x in I and
A4: y in J and
A5: w = [x,y] by A1,ZFMISC_1:def 2;
    f.w in Int G & f.(x,y) = y by A3,A4,CONNSP_2:def 1,FUNCT_3:def 5;
    then w in Int H by A3,A5,A2,ZFMISC_1:def 2;
    then reconsider H as a_neighborhood of w by CONNSP_2:def 1;
    take H;
    reconsider X = Int G as non empty Subset of T by CONNSP_2:def 1;
    [:[#]S,X:] <> {};
    then f.:H = Int G by EQREL_1:49;
    hence thesis by TOPS_1:16;
  end;
  hence thesis;
end;

theorem Th41:
  for f being continuous Function of T, S, g being continuous
  Function of T, R holds <:f,g:> is continuous Function of T, [:S,R:]
proof
  let f be continuous Function of T, S, g be continuous Function of T, R;
A1: <:f,g:> = [:f,g:]*(delta the carrier of T) by FUNCT_3:78;
  delta the carrier of T is continuous Function of T,[:T,T:] by Th38;
  hence thesis by A1;
end;

theorem Th42:
  <:pr2(the carrier of S,the carrier of T), pr1(the carrier of S,
  the carrier of T):> is continuous Function of [:S,T:],[:T,S:]
proof
  pr1(the carrier of S,the carrier of T) is continuous Function of [:S,T:]
,S & pr2(the carrier of S,the carrier of T) is continuous Function of [:S,T:],T
  by Th39,Th40;
  hence thesis by Th41;
end;

theorem Th43:
  for f being Function of [:S,T:], [:T,S:] st f = <:pr2(the
carrier of S,the carrier of T), pr1(the carrier of S,the carrier of T):> holds
  f is being_homeomorphism
proof
  let f be Function of [:S,T:], [:T,S:] such that
A1: f = <:pr2(the carrier of S,the carrier of T), pr1(the carrier of S,
  the carrier of T):>;
  thus dom f = [#][:S,T:] by FUNCT_2:def 1;
  thus
A2: rng f = [:the carrier of T,the carrier of S:] by A1,Th4
    .= [#][:T,S:] by BORSUK_1:def 2;
  thus
 f is one-to-one by A1;
  thus f is continuous by A1,Th42;
  f is onto by A2,FUNCT_2:def 3;
  then f" = (f qua Function)" by A1,TOPS_2:def 4
    .= <:pr2(the carrier of T,the carrier of S), pr1(the carrier of T,the
  carrier of S):> by A1,Th8;
  hence thesis by Th42;
end;

theorem
  [:S,T:], [:T,S:] are_homeomorphic
proof
  reconsider f = <:pr2(the carrier of S,the carrier of T), pr1(the carrier of
  S,the carrier of T):> as Function of [:S,T:], [:T,S:] by Th42;
  take f;
  thus thesis by Th43;
end;

theorem Th45:
  for T being Hausdorff non empty TopSpace for f, g being
continuous Function of S, T holds (for X being Subset of S st X = {p where p is
  Point of S: f.p <> g.p} holds X is open) & for X being Subset of S st X = {p
  where p is Point of S: f.p = g.p} holds X is closed
proof
  let T be Hausdorff non empty TopSpace, f, g be continuous Function of S, T;
  {p where p is Point of S: f.p <> g.p} c= the carrier of S
  proof
    let x be object;
    assume x in {p where p is Point of S: f.p <> g.p};
    then ex a being Point of S st x = a & f.a <> g.a;
    hence thesis;
  end;
  then reconsider A = {p where p is Point of S: f.p <> g.p} as Subset of S;
A1: [#]T <> {};
  thus for X being Subset of S st X = {p where p is Point of S: f.p <> g.p
  } holds X is open
  proof
    let X be Subset of S such that
A2: X = {p where p is Point of S: f.p <> g.p};
    for x being set holds x in X iff ex Q being Subset of S st Q is open &
    Q c= X & x in Q
    proof
      let x be set;
      hereby
        assume x in X;
        then consider p being Point of S such that
A3:     x = p and
A4:     f.p <> g.p by A2;
        consider W, V being Subset of T such that
A5:     W is open & V is open and
A6:     f.p in W and
A7:     g.p in V and
A8:     W misses V by A4,PRE_TOPC:def 10;
        dom g = the carrier of S by FUNCT_2:def 1;
        then [x,g.p] in g by A3,FUNCT_1:def 2;
        then
A9:     x in g"V by A7,RELAT_1:def 14;
        take Q = (f"W) /\ (g"V);
        f"W is open & g"V is open by A1,A5,TOPS_2:43;
        hence Q is open;
        thus Q c= X
        proof
          let q be object;
          assume
A10:      q in Q;
          then q in f"W by XBOOLE_0:def 4;
          then consider yf being object such that
A11:      [q,yf] in f and
A12:      yf in W by RELAT_1:def 14;
          q in g"V by A10,XBOOLE_0:def 4;
          then consider yg being object such that
A13:      [q,yg] in g & yg in V by RELAT_1:def 14;
A14:      yg = g.q & not yg in W by A8,A13,FUNCT_1:1,XBOOLE_0:3;
          yf = f.q by A11,FUNCT_1:1;
          hence thesis by A2,A10,A12,A14;
        end;
        dom f = the carrier of S by FUNCT_2:def 1;
        then [x,f.p] in f by A3,FUNCT_1:def 2;
        then x in f"W by A6,RELAT_1:def 14;
        hence x in Q by A9,XBOOLE_0:def 4;
      end;
      given Q being Subset of S such that
      Q is open and
A15:  Q c= X & x in Q;
      thus thesis by A15;
    end;
    hence thesis by TOPS_1:25;
  end;
  then
A16: A is open;
  let X be Subset of S such that
A17: X = {p where p is Point of S: f.p = g.p};
  X` = A
  proof
    hereby
      let x be object;
      assume
A18:  x in X`;
      then not x in X by XBOOLE_0:def 5;
      then f.x <> g.x by A17,A18;
      hence x in A by A18;
    end;
    let x be object;
    assume x in A;
    then consider p being Point of S such that
A19: x = p and
A20: f.p <> g.p;
    now
      assume p in {t where t is Point of S: f.t = g.t};
      then ex t being Point of S st p = t & f.t = g.t;
      hence contradiction by A20;
    end;
    hence thesis by A17,A19,XBOOLE_0:def 5;
  end;
  hence thesis by A16;
end;

theorem
  T is Hausdorff iff for A being Subset of [:T,T:] st A = id the carrier
  of T holds A is closed
proof
  reconsider f = pr1(the carrier of T,the carrier of T), g = pr2(the carrier
  of T,the carrier of T) as continuous Function of [:T,T:],T by Th39,Th40;
  reconsider A = id the carrier of T as Subset of [:T,T:] by BORSUK_1:def 2;
  hereby
    assume
A1: T is Hausdorff;
    let A be Subset of [:T,T:];
    assume A = id the carrier of T;
    then A = {p where p is Point of [:T,T:]: f.p = g.p} by Th37;
    hence A is closed by A1,Th45;
  end;
  assume
  for A being Subset of [:T,T:] st A = id the carrier of T holds A is closed;
  then [#][:T,T:] = [:[#]T,[#]T:] & A is closed by BORSUK_1:def 2;
  then [:[#]T,[#]T:] \ A is open;
  then consider SF being Subset-Family of [:T,T:] such that
A2: [:[#]T,[#]T:] \ A = union SF and
A3: for e being set st e in SF ex X1, Y1 being Subset of T st e = [:X1,
  Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
  let p, q be Point of T;
  assume not p = q;
  then
  the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] & not [p
  ,q] in id [#]T by BORSUK_1:def 2,RELAT_1:def 10;
  then [p,q] in [:[#]T,[#]T:] \ A by XBOOLE_0:def 5;
  then consider XY being set such that
A4: [p,q] in XY and
A5: XY in SF by A2,TARSKI:def 4;
  consider X1, Y1 being Subset of T such that
A6: XY = [:X1,Y1:] and
A7: X1 is open & Y1 is open by A3,A5;
  take X1, Y1;
  thus X1 is open & Y1 is open by A7;
  thus p in X1 & q in Y1 by A4,A6,ZFMISC_1:87;
  assume X1 /\ Y1 <> {};
  then consider w being object such that
A8: w in X1 /\ Y1 by XBOOLE_0:def 1;
  w in X1 & w in Y1 by A8,XBOOLE_0:def 4;
  then [w,w] in XY by A6,ZFMISC_1:87;
  then [w,w] in union SF by A5,TARSKI:def 4;
  then not [w,w] in A by A2,XBOOLE_0:def 5;
  hence contradiction by A8,RELAT_1:def 10;
end;

registration
  let S, T be TopStruct;
  cluster strict for Refinement of S, T;
  existence
  proof
    set R = the Refinement of S, T;
    set R1 = the TopStruct of R;
    (the topology of S) \/ (the topology of T) is prebasis of R by
YELLOW_9:def 6;
    then the carrier of R1 = (the carrier of S) \/ (the carrier of T) & (the
topology of S) \/ (the topology of T) is prebasis of R1 by Th33,YELLOW_9:def 6;
    then reconsider R1 as Refinement of S, T by YELLOW_9:def 6;
    take R1;
    thus thesis;
  end;
end;

registration
  let S be non empty TopStruct, T be TopStruct;
  cluster strict non empty for Refinement of S, T;
  existence
  proof
    set R = the strict Refinement of S, T;
    take R;
    thus thesis;
  end;
  cluster strict non empty for Refinement of T, S;
  existence
  proof
    set R = the strict Refinement of T, S;
    take R;
    thus thesis;
  end;
end;

theorem
  for R, S, T being TopStruct holds R is Refinement of S, T iff the
  TopStruct of R is Refinement of S, T
proof
  let R, S, T be TopStruct;
  hereby
    assume
A1: R is Refinement of S, T;
    then reconsider R1 = R as TopSpace;
    (the topology of S) \/ (the topology of T) is prebasis of R by A1,
YELLOW_9:def 6;
    then
A2: (the topology of S) \/ (the topology of T) is prebasis of the TopStruct
    of R1 by Th33;
    the carrier of the TopStruct of R1 = (the carrier of S) \/ (the
    carrier of T) by A1,YELLOW_9:def 6;
    hence the TopStruct of R is Refinement of S, T by A2,YELLOW_9:def 6;
  end;
  assume
A3: the TopStruct of R is Refinement of S, T;
  then reconsider R1 = R as TopSpace by TEX_2:7;
  (the topology of S) \/ (the topology of T) is prebasis of the TopStruct
  of R by A3,YELLOW_9:def 6;
  then
A4: (the topology of S) \/ (the topology of T) is prebasis of R1 by Th33;
  the carrier of R1 = (the carrier of S) \/ (the carrier of T) by A3,
YELLOW_9:def 6;
  hence thesis by A4,YELLOW_9:def 6;
end;

reserve S1, S2, T1, T2 for non empty TopSpace,
  R for Refinement of [:S1,T1:], [:S2,T2:],
  R1 for Refinement of S1, S2,
  R2 for Refinement of T1, T2;

theorem Th48:
  the carrier of S1 = the carrier of S2 & the carrier of T1 = the
carrier of T2 implies { [:U1,V1:] /\ [:U2,V2:] where U1 is Subset of S1, U2 is
Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : U1 is open & U2 is open
  & V1 is open & V2 is open } is Basis of R
proof
  assume
A1: the carrier of S1 = the carrier of S2 & the carrier of T1 = the
  carrier of T2;
  set Y = { [:U1,V1:] /\ [:U2,V2:] where U1 is Subset of S1, U2 is Subset of
  S2, V1 is Subset of T1, V2 is Subset of T2 : U1 is open & U2 is open & V1 is
  open & V2 is open };
A2: the carrier of [:S2,T2:] = [:the carrier of S2, the carrier of T2:] by
BORSUK_1:def 2;
A3: the carrier of [:S1,T1:] = [:the carrier of S1, the carrier of T1:] by
BORSUK_1:def 2;
  then reconsider
  BST = INTERSECTION(the topology of [:S1,T1:], the topology of [:
  S2,T2:]) as Basis of R by A1,A2,YELLOW_9:60;
A4: the carrier of R = (the carrier of [:S1,T1:]) \/ the carrier of [:S2,T2
  :] by YELLOW_9:def 6
    .= [:the carrier of S1,the carrier of T1:] \/ [:the carrier of S2,the
  carrier of T2:] by A3,BORSUK_1:def 2
    .= [:the carrier of S1,the carrier of T1:] by A1;
  Y c= bool the carrier of R
  proof
    let c be object;
    assume c in Y;
    then
    ex U1 being Subset of S1, U2 being Subset of S2, V1 being Subset of T1
, V2 being Subset of T2 st c = [:U1,V1:] /\ [:U2,V2:] & U1 is open & U2 is open
    & V1 is open & V2 is open;
    hence thesis by A1,A2,A4;
  end;
  then reconsider C1 = Y as Subset-Family of R;
  reconsider C1 as Subset-Family of R;
A5: the topology of [:S2,T2:] = { union A where A is Subset-Family of [:S2,
T2:]: A c= { [:X1,Y1:] where X1 is Subset of S2, Y1 is Subset of T2 : X1 in the
  topology of S2 & Y1 in the topology of T2}} by BORSUK_1:def 2;
A6: the topology of [:S1,T1:] = { union A where A is Subset-Family of [:S1,
T1:]: A c= { [:X1,Y1:] where X1 is Subset of S1, Y1 is Subset of T1 : X1 in the
  topology of S1 & Y1 in the topology of T1}} by BORSUK_1:def 2;
A7: for A being Subset of R st A is open for p being Point of R st p in A
  ex a being Subset of R st a in C1 & p in a & a c= A
  proof
    let A be Subset of R such that
A8: A is open;
    let p be Point of R;
    assume p in A;
    then consider X being Subset of R such that
A9: X in BST and
A10: p in X and
A11: X c= A by A8,YELLOW_9:31;
    consider X1, X2 be set such that
A12: X1 in the topology of [:S1,T1:] and
A13: X2 in the topology of [:S2,T2:] and
A14: X = X1 /\ X2 by A9,SETFAM_1:def 5;
    consider F1 being Subset-Family of [:S1,T1:] such that
A15: X1 = union F1 and
A16: F1 c= { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 :
    K1 in the topology of S1 & L1 in the topology of T1 } by A6,A12;
    p in X1 by A10,A14,XBOOLE_0:def 4;
    then consider G1 being set such that
A17: p in G1 and
A18: G1 in F1 by A15,TARSKI:def 4;
A19: G1 in { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 : K1
    in the topology of S1 & L1 in the topology of T1 } by A16,A18;
    consider F2 being Subset-Family of [:S2,T2:] such that
A20: X2 = union F2 and
A21: F2 c= { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 :
    K2 in the topology of S2 & L2 in the topology of T2 } by A5,A13;
    p in X2 by A10,A14,XBOOLE_0:def 4;
    then consider G2 being set such that
A22: p in G2 and
A23: G2 in F2 by A20,TARSKI:def 4;
    G2 in { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 : K2
    in the topology of S2 & L2 in the topology of T2 } by A21,A23;
    then consider K2 being Subset of S2, L2 being Subset of T2 such that
A24: G2 = [:K2,L2:] and
A25: K2 in the topology of S2 & L2 in the topology of T2;
A26: [:K2,L2:] c= X2 by A20,A23,A24,ZFMISC_1:74;
A27: K2 is open & L2 is open by A25;
    consider K1 being Subset of S1, L1 being Subset of T1 such that
A28: G1 = [:K1,L1:] and
A29: K1 in the topology of S1 & L1 in the topology of T1 by A19;
    reconsider a = [:K1,L1:] /\ [:K2,L2:] as Subset of R by A1,A4,
BORSUK_1:def 2;
    take a;
    K1 is open & L1 is open by A29;
    hence a in C1 by A27;
    thus p in a by A17,A22,A28,A24,XBOOLE_0:def 4;
    [:K1,L1:] c= X1 by A15,A18,A28,ZFMISC_1:74;
    then a c= X by A14,A26,XBOOLE_1:27;
    hence thesis by A11;
  end;
  Y c= the topology of R
  proof
    let c be object;
A30: BST c= the topology of R by TOPS_2:64;
    assume c in Y;
    then consider
    U1 being Subset of S1, U2 being Subset of S2, V1 being Subset of
    T1, V2 being Subset of T2 such that
A31: c = [:U1,V1:] /\ [:U2,V2:] and
A32: U1 is open and
A33: U2 is open and
A34: V1 is open and
A35: V2 is open;
    [:U2,V2:] is open by A33,A35,BORSUK_1:6;
    then
A36: [:U2,V2:] in the topology of [:S2,T2:];
    [:U1,V1:] is open by A32,A34,BORSUK_1:6;
    then [:U1,V1:] in the topology of [:S1,T1:];
    then c in BST by A31,A36,SETFAM_1:def 5;
    hence thesis by A30;
  end;
  hence thesis by A7,YELLOW_9:32;
end;

theorem Th49:
  the carrier of S1 = the carrier of S2 & the carrier of T1 = the
  carrier of T2 implies the carrier of [:R1,R2:] = the carrier of R & the
  topology of [:R1,R2:] = the topology of R
proof
  assume that
A1: the carrier of S1 = the carrier of S2 and
A2: the carrier of T1 = the carrier of T2;
A3: the carrier of R1 = (the carrier of S1) \/ the carrier of S2 by
YELLOW_9:def 6
    .= the carrier of S1 by A1;
  set C = { [:U1,V1:] /\ [:U2,V2:] where U1 is Subset of S1, U2 is Subset of
  S2, V1 is Subset of T1, V2 is Subset of T2 : U1 is open & U2 is open & V1 is
  open & V2 is open };
  reconsider BT = INTERSECTION(the topology of T1, the topology of T2) as
  Basis of R2 by A2,YELLOW_9:60;
  reconsider BS = INTERSECTION(the topology of S1, the topology of S2) as
  Basis of R1 by A1,YELLOW_9:60;
  reconsider Bpr = {[:a,b:] where a is Subset of R1, b is Subset of R2: a in
  BS & b in BT} as Basis of [:R1,R2:] by YELLOW_9:40;
A4: C = Bpr
  proof
    hereby
      let c be object;
      assume c in C;
      then consider
      U1 being Subset of S1, U2 being Subset of S2, V1 being Subset
      of T1, V2 being Subset of T2 such that
A5:   c = [:U1,V1:] /\ [:U2,V2:] and
A6:   U1 is open & U2 is open and
A7:   V1 is open & V2 is open;
      U1 in the topology of S1 & U2 in the topology of S2 by A6;
      then
A8:   U1 /\ U2 in BS by SETFAM_1:def 5;
      V1 in the topology of T1 & V2 in the topology of T2 by A7;
      then
A9:   V1 /\ V2 in BT by SETFAM_1:def 5;
      c = [:U1 /\ U2, V1 /\ V2:] by A5,ZFMISC_1:100;
      hence c in Bpr by A8,A9;
    end;
    let c be object;
    assume c in Bpr;
    then consider a being Subset of R1, b being Subset of R2 such that
A10: c = [:a,b:] and
A11: a in BS and
A12: b in BT;
    consider a1, a2 being set such that
A13: a1 in the topology of S1 and
A14: a2 in the topology of S2 and
A15: a = a1 /\ a2 by A11,SETFAM_1:def 5;
    reconsider a2 as Subset of S2 by A14;
    reconsider a1 as Subset of S1 by A13;
A16: a1 is open & a2 is open by A13,A14;
    consider b1, b2 being set such that
A17: b1 in the topology of T1 and
A18: b2 in the topology of T2 and
A19: b = b1 /\ b2 by A12,SETFAM_1:def 5;
    reconsider b2 as Subset of T2 by A18;
    reconsider b1 as Subset of T1 by A17;
A20: b1 is open & b2 is open by A17,A18;
    c = [:a1,b1:] /\ [:a2,b2:] by A10,A15,A19,ZFMISC_1:100;
    hence thesis by A16,A20;
  end;
A21: the carrier of R2 = (the carrier of T1) \/ the carrier of T2 by
YELLOW_9:def 6
    .= the carrier of T1 by A2;
A22: the carrier of [:S1,T1:] = [:the carrier of S1, the carrier of T1:] by
BORSUK_1:def 2;
  the carrier of R = (the carrier of [:S1,T1:]) \/ the carrier of [:S2,T2
  :] by YELLOW_9:def 6
    .= [:the carrier of S1,the carrier of T1:] \/ [:the carrier of S2,the
  carrier of T2:] by A22,BORSUK_1:def 2
    .= [:the carrier of S1,the carrier of T1:] by A1,A2;
  hence
A23: the carrier of [:R1,R2:] = the carrier of R by A3,A21,BORSUK_1:def 2;
  C is Basis of R by A1,A2,Th48;
  hence thesis by A23,A4,YELLOW_9:25;
end;

theorem
  the carrier of S1 = the carrier of S2 & the carrier of T1 = the
  carrier of T2 implies [:R1,R2:] is Refinement of [:S1,T1:], [:S2,T2:]
proof
  set R = the strict Refinement of [:S1,T1:], [:S2,T2:];
  assume
A1: the carrier of S1 = the carrier of S2 & the carrier of T1 = the
  carrier of T2;
  then the carrier of [:R1,R2:] = the carrier of R by Th49;
  hence thesis by A1,Th49;
end;