:: Properties of the Product of Compact Topological Spaces
::  by Adam Grabowski
::
:: Received February 13, 1999
:: Copyright (c) 1999-2018 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 PRE_TOPC, SUBSET_1, ZFMISC_1, XBOOLE_0, FUNCOP_1, ORDINAL2,
      FUNCT_1, RELAT_1, STRUCT_0, TOPS_2, T_0TOPSP, RCOMP_1, MCART_1, PARTFUN1,
      TARSKI, PBOOLE, BORSUK_1, TOPS_1, CONNSP_2, SETFAM_1, FINSET_1, FUNCT_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, FUNCT_1,
      PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, DOMAIN_1,
      STRUCT_0, PRE_TOPC, TOPS_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP,
      FINSET_1, FUNCT_3, CONNSP_2;
 constructors FUNCT_3, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, T_0TOPSP, FUNCOP_1,
      BINOP_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC,
      TOPS_1, BORSUK_1, COMPTS_1, BORSUK_2, ZFMISC_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, TOPS_2, COMPTS_1, T_0TOPSP, FUNCT_1, XBOOLE_0;
 equalities BINOP_1, STRUCT_0;
 expansions TARSKI, TOPS_2, COMPTS_1, T_0TOPSP, XBOOLE_0;
 theorems BORSUK_1, FUNCOP_1, TOPS_2, FUNCT_2, FUNCT_1, PRE_TOPC, TARSKI,
      TOPS_1, TOPMETR, ZFMISC_1, CONNSP_2, FUNCT_3, COMPTS_1, FINSET_1,
      YELLOW12, TSEP_1, TOPGRP_1, XBOOLE_0, XBOOLE_1, SETFAM_1;
 schemes PBOOLE, CLASSES1, XFAMILY;

begin :: Preliminaries

theorem
  for S, T being TopSpace holds [#][:S, T:] = [:[#]S, [#]T:] by BORSUK_1:def 2;

theorem Th2:
  for X, Y being non empty TopSpace, x being Point of X holds Y -->
  x is continuous Function of Y, X|{x}
proof
  let X, Y be non empty TopSpace, x be Point of X;
  set Z = {x};
  set f = Y --> x;
  x in Z & the carrier of (X|Z) = Z by PRE_TOPC:8,TARSKI:def 1;
  then reconsider g = f as Function of Y, X|Z by FUNCOP_1:45;
  g is continuous by TOPMETR:6;
  hence thesis;
end;

registration
  let T be TopStruct;
  cluster id T -> being_homeomorphism;
  coherence by TOPGRP_1:20;
end;

Lm1: for S being TopStruct holds S, S are_homeomorphic
proof
  let S be TopStruct;
  take id S;
  thus thesis;
end;

Lm2: for S, T being non empty TopStruct st S, T are_homeomorphic holds T, S
are_homeomorphic
proof
  let S, T be non empty TopStruct;
  assume S, T are_homeomorphic;
  then consider f being Function of S, T such that
A1: f is being_homeomorphism;
  f" is being_homeomorphism by A1,TOPS_2:56;
  hence thesis;
end;

definition
  let S, T be TopStruct;
  redefine pred S, T are_homeomorphic;
  reflexivity by Lm1;
end;

definition
  let S, T be non empty TopStruct;
  redefine pred S, T are_homeomorphic;
  reflexivity by Lm1;
  symmetry by Lm2;
end;

theorem
  for S, T, V being non empty TopSpace st S, T are_homeomorphic & T, V
  are_homeomorphic holds S, V are_homeomorphic
proof
  let S, T, V be non empty TopSpace;
  assume that
A1: S, T are_homeomorphic and
A2: T, V are_homeomorphic;
  consider f being Function of S, T such that
A3: f is being_homeomorphism by A1;
  consider g being Function of T, V such that
A4: g is being_homeomorphism by A2;
  g * f is being_homeomorphism by A3,A4,TOPS_2:57;
  hence thesis;
end;

begin :: On the projections and empty topological spaces

registration
  let T be TopStruct, P be empty Subset of T;
  cluster T | P -> empty;
  coherence;
end;

registration
  cluster empty -> compact for TopSpace;
  coherence;
end;

theorem Th4:
  for X, Y being non empty TopSpace, x being Point of X, f being
  Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f is
  one-to-one
proof
  let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | {
  x}:], Y;
  set Z = {x};
  assume
A1: f = pr1(the carrier of Y, Z);
  let z, y be object such that
A2: z in dom f and
A3: y in dom f and
A4: f.z = f.y;
A5: dom f = [:the carrier of Y, Z:] by A1,FUNCT_3:def 4;
  then consider x1, x2 being object such that
A6: x1 in the carrier of Y and
A7: x2 in Z and
A8: z = [x1, x2] by A2,ZFMISC_1:def 2;
  consider y1, y2 being object such that
A9: y1 in the carrier of Y and
A10: y2 in Z and
A11: y = [y1, y2] by A5,A3,ZFMISC_1:def 2;
A12: x2 = x by A7,TARSKI:def 1
    .= y2 by A10,TARSKI:def 1;
  x1 = f.(x1, x2) by A1,A6,A7,FUNCT_3:def 4
    .= f.(y1, y2) by A4,A8,A11
    .= y1 by A1,A9,A10,FUNCT_3:def 4;
  hence thesis by A8,A11,A12;
end;

theorem Th5:
  for X, Y being non empty TopSpace, x being Point of X, f being
  Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f is
  one-to-one
proof
  let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x},
  Y:], Y;
  set Z = {x};
  assume
A1: f = pr2(Z, the carrier of Y);
  let z, y be object such that
A2: z in dom f and
A3: y in dom f and
A4: f.z = f.y;
A5: dom f = [:Z, the carrier of Y:] by A1,FUNCT_3:def 5;
  then consider x1, x2 being object such that
A6: x1 in Z and
A7: x2 in the carrier of Y and
A8: z = [x1,x2] by A2,ZFMISC_1:def 2;
  consider y1, y2 being object such that
A9: y1 in Z and
A10: y2 in the carrier of Y and
A11: y = [y1,y2] by A5,A3,ZFMISC_1:def 2;
A12: x1 = x by A6,TARSKI:def 1
    .= y1 by A9,TARSKI:def 1;
  x2= f.(x1, x2) by A1,A6,A7,FUNCT_3:def 5
    .= f.(y1, y2) by A4,A8,A11
    .= y2 by A1,A9,A10,FUNCT_3:def 5;
  hence thesis by A8,A11,A12;
end;

theorem Th6:
  for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f" = <:id
  Y, Y --> x:>
proof
  let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | {
  x}:], Y;
  set Z = {x};
  set idZ = id Y;
A1: rng idZ c= the carrier of Y;
  assume
A2: f = pr1(the carrier of Y, Z);
  then
A3: rng f = the carrier of Y by FUNCT_3:44;
  reconsider Z as non empty Subset of X;
  reconsider idY = Y --> x as continuous Function of Y, (X|Z) by Th2;
  reconsider KA = <:idZ, idY:> as continuous Function of Y, [:Y, (X|Z):] by
YELLOW12:41;
A4: [:the carrier of Y, Z:] c= rng KA
  proof
    let y be object;
    assume y in [:the carrier of Y, Z:];
    then consider y1, y2 being object such that
A5: y1 in the carrier of Y and
A6: y2 in {x} & y = [y1,y2] by ZFMISC_1:def 2;
A7: y = [y1, x] by A6,TARSKI:def 1;
A8: idY.y1 = ((the carrier of Y) --> x).y1 .= x by A5,FUNCOP_1:7;
A9: y1 in dom KA by A5,FUNCT_2:def 1;
    then KA. y1 = [idZ.y1, idY.y1] by FUNCT_3:def 7
      .= [y1, x] by A5,A8,FUNCT_1:18;
    hence thesis by A7,A9,FUNCT_1:def 3;
  end;
  rng idY c= the carrier of (X|Z);
  then
A10: rng idY c= Z by PRE_TOPC:8;
  then rng KA c= [:rng idZ, rng idY:] & [:rng idZ, rng idY:] c= [:the carrier
  of Y, Z:] by FUNCT_3:51,ZFMISC_1:96;
  then rng KA c= [:the carrier of Y, Z:];
  then
A11: rng KA = [:the carrier of Y, Z:] by A4
    .= dom f by A2,FUNCT_3:def 4;
A12: f is one-to-one by A2,Th4;
A13: f is onto by A3,FUNCT_2:def 3;
  dom idY = the carrier of Y by FUNCT_2:def 1
    .= dom idZ by FUNCT_2:def 1;
  then f*KA = id rng f by A2,A3,A10,A1,FUNCT_3:52;
  then KA = (f qua Function)" by A12,A11,FUNCT_1:42;
  hence thesis by A12,A13,TOPS_2:def 4;
end;

theorem Th7:
  for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f" = <:Y
  --> x, id Y:>
proof
  let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x},
  Y:], Y;
  set Z = {x};
  set idY = id Y;
A1: rng idY c= the carrier of Y;
  assume
A2: f = pr2(Z, the carrier of Y);
  then
A3: rng f = the carrier of Y by FUNCT_3:46;
  reconsider Z as non empty Subset of X;
  reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2;
  reconsider KA = <:idZ, idY:> as continuous Function of Y, [:(X|Z), Y:] by
YELLOW12:41;
A4: [:{x}, the carrier of Y:] c= rng KA
  proof
    let y be object;
    assume y in [:{x}, the carrier of Y:];
    then consider y1, y2 being object such that
A5: y1 in {x} and
A6: y2 in the carrier of Y and
A7: y = [y1,y2] by ZFMISC_1:def 2;
A8: y = [x, y2] by A5,A7,TARSKI:def 1;
A9: idZ.y2 = ((the carrier of Y) --> x).y2 .= x by A6,FUNCOP_1:7;
A10: y2 in dom KA by A6,FUNCT_2:def 1;
    then KA. y2 = [idZ.y2, idY.y2] by FUNCT_3:def 7
      .= [x, y2] by A6,A9,FUNCT_1:18;
    hence thesis by A8,A10,FUNCT_1:def 3;
  end;
  rng idZ c= the carrier of (X|Z);
  then
A11: rng idZ c= Z by PRE_TOPC:8;
  then rng KA c= [:rng idZ, rng idY:] & [:rng idZ, rng idY:] c= [:{x},the
  carrier of Y:] by FUNCT_3:51,ZFMISC_1:96;
  then rng KA c= [:{x}, the carrier of Y:];
  then
A12: rng KA = [:Z, the carrier of Y:] by A4
    .= dom f by A2,FUNCT_3:def 5;
A13: f is one-to-one by A2,Th5;
A14: f is onto by A3,FUNCT_2:def 3;
  dom idZ = the carrier of Y by FUNCT_2:def 1
    .= dom idY by FUNCT_2:def 1;
  then f*KA = id rng f by A2,A3,A11,A1,FUNCT_3:52;
  then KA = (f qua Function)" by A13,A12,FUNCT_1:42;
  hence thesis by A13,A14,TOPS_2:def 4;
end;

theorem
  for X, Y being non empty TopSpace, x being Point of X, f being
  Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f is
  being_homeomorphism
proof
  let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | {
  x}:], Y;
  set Z = {x};
  assume
A1: f = pr1(the carrier of Y, Z);
  thus dom f = [#][:Y, (X|Z):] by FUNCT_2:def 1;
  thus rng f = [#]Y by A1,FUNCT_3:44;
  thus f is one-to-one by A1,Th4;
  the carrier of (X|Z) = Z by PRE_TOPC:8;
  hence f is continuous by A1,YELLOW12:39;
  reconsider Z as non empty Subset of X;
  reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2;
  reconsider KA = <:id Y, idZ:> as continuous Function of Y, [:Y, (X|Z):] by
YELLOW12:41;
  KA = f" by A1,Th6;
  hence thesis;
end;

theorem Th9:
  for X, Y being non empty TopSpace, x being Point of X, f being
  Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f is
  being_homeomorphism
proof
  let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x},
  Y:], Y;
  set Z = {x};
  assume
A1: f = pr2(Z, the carrier of Y);
  thus dom f = [#][:(X|Z), Y:] by FUNCT_2:def 1;
  thus rng f = [#]Y by A1,FUNCT_3:46;
  thus f is one-to-one by A1,Th5;
  the carrier of (X|Z) = Z by PRE_TOPC:8;
  hence f is continuous by A1,YELLOW12:40;
  reconsider Z as non empty Subset of X;
  reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2;
  reconsider KA = <:idZ, id Y:> as continuous Function of Y, [:(X|Z), Y:] by
YELLOW12:41;
  KA = f" by A1,Th7;
  hence thesis;
end;

begin :: On the product of compact spaces

theorem
  for X being non empty TopSpace, Y being compact non empty TopSpace, G
being open Subset of [:X, Y:], x being set st [:{x}, the carrier of Y:] c= G ex
  f being ManySortedSet of the carrier of Y st
  for i being object st i in the
carrier of Y ex G1 being Subset of X, H1 being Subset of Y st f.i = [G1,H1] & [
  x, i] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G
proof
  let X be non empty TopSpace, Y be compact non empty TopSpace, G be open
  Subset of [:X, Y:], x be set;
  set y = the Point of Y;
A1: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] & [x,y]
  in [:{x},the carrier of Y:] by BORSUK_1:def 2,ZFMISC_1:105;
  defpred P[object,object] means
   ex G1 be Subset of X, H1 be Subset of Y st $2 = [
  G1,H1] & [x, $1] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G;
  assume
A2: [:{x}, the carrier of Y:] c= G;
  then [:{x}, the carrier of Y:] c= the carrier of [:X,Y:] by XBOOLE_1:1;
  then reconsider x9 = x as Point of X by A1,ZFMISC_1:87;
A3: [:{x9}, the carrier of Y:] c= union Base-Appr G by A2,BORSUK_1:13;
A4: now
    let y be set;
A5: x in {x9} by TARSKI:def 1;
    assume y in the carrier of Y;
    then [x,y] in [:{x9}, the carrier of Y:] by A5,ZFMISC_1:87;
    then consider Z be set such that
A6: [x, y] in Z and
A7: Z in Base-Appr G by A3,TARSKI:def 4;
    Base-Appr G = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y:
    [:X1,Y1:] c= G & X1 is open & Y1 is open} by BORSUK_1:def 3;
    then ex X1 be Subset of X, Y1 be Subset of Y st Z = [:X1, Y1:] & [:X1,Y1:]
    c= G & X1 is open & Y1 is open by A7;
    hence ex G1 be Subset of X, H1 be Subset of Y st [x, y] in [:G1, H1:] & [:
    G1,H1:] c= G & G1 is open & H1 is open by A6;
  end;
A8: for i be object st i in the carrier of Y ex j be object st P[i,j]
  proof
    let i be object;
    assume i in the carrier of Y;
    then consider G1 be Subset of X, H1 be Subset of Y such that
A9: [x, i] in [:G1, H1:] & [:G1, H1:] c= G & G1 is open & H1 is open by A4;
    ex G2 be Subset of X, H2 be Subset of Y st [G1,H1] = [G2,H2] & [x, i]
    in [:G2, H2:] & G2 is open & H2 is open & [:G2, H2:] c= G by A9;
    hence thesis;
  end;
  ex f being ManySortedSet of the carrier of Y st for i be object st i in
  the carrier of Y holds P[i,f.i] from PBOOLE:sch 3 (A8 );
  hence thesis;
end;

theorem Th11:
  for X being non empty TopSpace, Y being compact non empty
TopSpace, G being open Subset of [:Y, X:] holds for x being set st [:[#]Y, {x}
:] c= G holds ex R be open Subset of X st x in R & R c= { y where y is Point of
X: [:[#]Y, {y}:] c= G }
proof
  let X be non empty TopSpace, Y be compact non empty TopSpace, G be open
  Subset of [:Y, X:];
  let x be set;
  set y = the Point of Y;
A1: the carrier of [:Y,X:] = [: the carrier of Y, the carrier of X:] & [y,x]
  in [:the carrier of Y,{x}:] by BORSUK_1:def 2,ZFMISC_1:106;
  assume
A2: [:[#]Y, {x}:] c= G;
  then [:[#]Y,{x}:] c= the carrier of [:Y,X:] by XBOOLE_1:1;
  then reconsider x9 = x as Point of X by A1,ZFMISC_1:87;
  Int G = G by TOPS_1:23;
  then [#]Y is compact & G is a_neighborhood of [:[#]Y, {x9}:] by A2,COMPTS_1:1
,CONNSP_2:def 2;
  then consider
  W being a_neighborhood of [#]Y, V being a_neighborhood of x9 such
  that
A3: [:W, V:] c= G by BORSUK_1:25;
  take R = Int V;
  Int W c= W & [#]Y c= Int W by CONNSP_2:def 2,TOPS_1:16;
  then
A4: [#]Y c= W;
A5: Int V c= V by TOPS_1:16;
  R c= { z where z is Point of X : [:[#]Y, {z}:] c= G }
  proof
    let r be object;
    assume
A6: r in R;
    then reconsider r9 = r as Point of X;
    {r} c= V by A5,A6,ZFMISC_1:31;
    then [:[#]Y, {r9}:] c= [:W, V:] by A4,ZFMISC_1:96;
    then [:[#]Y, {r9}:] c= G by A3;
    hence thesis;
  end;
  hence thesis by CONNSP_2:def 1;
end;

theorem Th12:
  for X being non empty TopSpace, Y being compact non empty
TopSpace, G being open Subset of [:Y, X:] holds { x where x is Point of X : [:
  [#]Y, {x}:] c= G } in the topology of X
proof
  let X be non empty TopSpace, Y be compact non empty TopSpace, G be open
  Subset of [:Y, X:];
  set Q = { x where x is Point of X : [:[#]Y, {x}:] c= G };
  Q c= the carrier of X
  proof
    let q be object;
    assume q in Q;
    then ex x9 being Point of X st q = x9 & [:[#]Y, {x9}:] c= G;
    hence thesis;
  end;
  then reconsider Q as Subset of X;
  defpred P[set] means ex y be set st y in Q & ex S be Subset of X st S = $1 &
  S is open & y in S & S c= Q;
  consider RR be set such that
A1: for x be set holds x in RR iff x in bool Q & P[x] from XFAMILY:sch
  1;
  RR c= bool Q
  by A1;
  then reconsider RR as Subset-Family of Q;
  Q c= union RR
  proof
    let a be object;
    assume a in Q;
    then ex x9 being Point of X st a = x9 & [:[#]Y, {x9}:] c= G;
    then consider R be open Subset of X such that
A2: a in R and
A3: R c= Q by Th11;
    R in RR by A1,A2,A3;
    hence thesis by A2,TARSKI:def 4;
  end;
  then
A4: union RR = Q;
  bool Q c= bool the carrier of X by ZFMISC_1:67;
  then reconsider RR as Subset-Family of X by XBOOLE_1:1;
  RR c= the topology of X
  proof
    let x be object;
    assume x in RR;
    then ex y be set st y in Q & ex S be Subset of X st S = x & S is open & y
    in S & S c= Q by A1;
    hence thesis by PRE_TOPC:def 2;
  end;
  hence thesis by A4,PRE_TOPC:def 1;
end;

theorem Th13:
  for X, Y being non empty TopSpace, x being Point of X holds [: X
  | {x}, Y :], Y are_homeomorphic
proof
  let X be non empty TopSpace, Y be non empty TopSpace, x be Point of X;
  set Z = {x};
  the carrier of [:(X|Z), Y:] = [:the carrier of (X|Z), the carrier of Y
  :] by BORSUK_1:def 2
    .= [:Z, the carrier of Y:] by PRE_TOPC:8;
  then reconsider f= pr2(Z, the carrier of Y) as Function of [:X|Z, Y:], Y;
  take f;
  thus thesis by Th9;
end;

Lm3: for X being non empty TopSpace, Y being non empty TopSpace, x being Point
of X, Z being non empty Subset of X st Z = {x} holds [: Y, X | Z :], Y
are_homeomorphic
proof
  let X be non empty TopSpace, Y be non empty TopSpace, x be Point of X, Z be
  non empty Subset of X;
  [: Y, X | Z :], [: X | Z, Y :] are_homeomorphic by YELLOW12:44;
  then consider g being Function of [: Y, X | Z :], [: X | Z, Y :] such that
A1: g is being_homeomorphism;
  assume Z = {x};
  then [: X | Z, Y :], Y are_homeomorphic by Th13;
  then consider f being Function of [: X | Z, Y :], Y such that
A2: f is being_homeomorphism;
  reconsider gf = f * g as Function of [: Y, X | Z :], Y;
  gf is being_homeomorphism by A2,A1,TOPS_2:57;
  hence thesis;
end;

theorem Th14:
  for S, T being non empty TopSpace st S, T are_homeomorphic & S
  is compact holds T is compact
proof
  let S, T be non empty TopSpace;
  assume that
A1: S, T are_homeomorphic and
A2: S is compact;
  consider f being Function of S, T such that
A3: f is being_homeomorphism by A1;
  f is continuous & rng f = [#] T by A3;
  hence thesis by A2,COMPTS_1:14;
end;

theorem Th15:
  for X, Y being TopSpace, XV being SubSpace of X holds [:Y, XV:]
  is SubSpace of [:Y, X:]
proof
  let X, Y be TopSpace, XV be SubSpace of X;
  set S = [:Y, XV:], T = [:Y, X:];
A1: the carrier of [:Y, XV:] = [:the carrier of Y, the carrier of XV:] by
BORSUK_1:def 2;
A2: the carrier of [:Y, X:] = [:the carrier of Y, the carrier of X:] & the
  carrier of XV c= the carrier of X by BORSUK_1:1,def 2;
A3: for P being Subset of S holds P in the topology of S iff ex Q being
  Subset of T st Q in the topology of T & P = Q /\ [#]S
  proof
    reconsider oS = [#]S as Subset of T by A1,A2,ZFMISC_1:96;
    let P be Subset of S;
    reconsider P9 = P as Subset of S;
    hereby
      assume P in the topology of S;
      then P9 is open by PRE_TOPC:def 2;
      then consider A being Subset-Family of S such that
A4:   P9 = union A and
A5:   for e be set st e in A ex X1 being Subset of Y, Y1 being Subset
      of XV st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
      set AA = {[:X1, Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1
being Subset of XV st Y1 = Y2 /\ [#](XV) & X1 is open & Y2 is open & [:X1, Y1:]
      in A };
      AA c= bool the carrier of T
      proof
        let a be object;
        assume a in AA;
        then
        ex Xx1 being Subset of Y, Yy2 being Subset of X st a = [: Xx1, Yy2
:] & ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open & Yy2 is
        open & [:Xx1, Y1:] in A;
        hence thesis;
      end;
      then reconsider AA as Subset-Family of T;
      reconsider AA as Subset-Family of T;
A6:   P c= union AA /\ [#]S
      proof
        let p be object;
        assume p in P;
        then consider A1 be set such that
A7:     p in A1 and
A8:     A1 in A by A4,TARSKI:def 4;
        reconsider A1 as Subset of S by A8;
        consider X2 being Subset of Y, Y2 being Subset of XV such that
A9:     A1 = [:X2,Y2:] and
A10:    X2 is open and
A11:    Y2 is open by A5,A8;
        Y2 in the topology of XV by A11,PRE_TOPC:def 2;
        then consider Q1 being Subset of X such that
A12:    Q1 in the topology of X and
A13:    Y2 = Q1 /\ [#]XV by PRE_TOPC:def 4;
        consider p1, p2 being object such that
A14:    p1 in X2 and
A15:    p2 in Y2 and
A16:    p = [p1, p2] by A7,A9,ZFMISC_1:def 2;
        reconsider Q1 as Subset of X;
        set EX = [:X2, Q1:];
        p2 in Q1 by A15,A13,XBOOLE_0:def 4;
        then
A17:    p in EX by A14,A16,ZFMISC_1:87;
        Q1 is open by A12,PRE_TOPC:def 2;
        then
        EX in {[:Xx1, Yy2:] where Xx1 is Subset of Y, Yy2 is Subset of X:
ex Z1 being Subset of XV st Z1 = Yy2 /\ [#](XV) & Xx1 is open & Yy2 is open &
        [:Xx1, Z1:] in A } by A8,A9,A10,A13;
        then p in union AA by A17,TARSKI:def 4;
        hence thesis by A7,A8,XBOOLE_0:def 4;
      end;
      AA c= the topology of T
      proof
        let t be object;
        set A9 = { t };
        assume t in AA;
        then consider Xx1 being Subset of Y, Yy2 being Subset of X such that
A18:    t = [:Xx1, Yy2:] and
A19:    ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open
        & Yy2 is open & [:Xx1, Y1:] in A;
        A9 c= bool the carrier of T
        proof
          let a be object;
          assume a in A9;
          then a = t by TARSKI:def 1;
          hence thesis by A18;
        end;
        then reconsider A9 as Subset-Family of T;
A20:    A9 c= { [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : X1
        in the topology of Y & Y1 in the topology of X }
        proof
          let x be object;
          assume x in A9;
          then
A21:      x = [:Xx1,Yy2:] by A18,TARSKI:def 1;
          Xx1 in the topology of Y & Yy2 in the topology of X by A19,
PRE_TOPC:def 2;
          hence thesis by A21;
        end;
        t = union A9;
        then t in { union As where As is Subset-Family of T : As c= { [:X1,Y1
:] where X1 is Subset of Y, Y1 is Subset of X : X1 in the topology of Y & Y1 in
        the topology of X}} by A20;
        hence thesis by BORSUK_1:def 2;
      end;
      then
A22:  union AA in the topology of T by PRE_TOPC:def 1;
      union AA /\ [#]S c= P
      proof
        let h be object;
        assume
A23:    h in union AA /\ [#]S;
        then h in union AA by XBOOLE_0:def 4;
        then consider A2 being set such that
A24:    h in A2 and
A25:    A2 in AA by TARSKI:def 4;
        consider Xx1 being Subset of Y, Yy2 being Subset of X such that
A26:    A2 = [:Xx1, Yy2:] and
A27:    ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open
        & Yy2 is open & [:Xx1, Y1:] in A by A25;
        consider Yy1 being Subset of XV such that
A28:    Yy1 = Yy2 /\ [#](XV) and
        Xx1 is open and
        Yy2 is open and
A29:    [:Xx1, Yy1:] in A by A27;
        consider p1, p2 being object such that
A30:    p1 in Xx1 and
A31:    p2 in Yy2 and
A32:    h = [p1, p2] by A24,A26,ZFMISC_1:def 2;
        p2 in the carrier of XV by A1,A23,A32,ZFMISC_1:87;
        then p2 in Yy2 /\ [#]XV by A31,XBOOLE_0:def 4;
        then h in [:Xx1, Yy1:] by A30,A32,A28,ZFMISC_1:87;
        hence thesis by A4,A29,TARSKI:def 4;
      end;
      then P = union AA /\ [#]S by A6;
      hence
      ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S by A22;
    end;
    given Q being Subset of T such that
A33: Q in the topology of T and
A34: P = Q /\ [#]S;
    reconsider Q9 = Q as Subset of T;
    Q9 is open by A33,PRE_TOPC:def 2;
    then consider A being Subset-Family of T such that
A35: Q9 = union A and
A36: for e be set st e in A ex X1 being Subset of Y, Y1 being Subset
    of X st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
    reconsider A as Subset-Family of T;
    reconsider AA = A | oS as Subset-Family of T|oS;
    reconsider AA as Subset-Family of S by PRE_TOPC:8;
    reconsider AA as Subset-Family of S;
A37: for e be set st e in AA ex X1 being Subset of Y, Y1 being Subset of
    XV st e = [:X1,Y1:] & X1 is open & Y1 is open
    proof
      let e be set;
      assume
A38:  e in AA;
      then reconsider e9 = e as Subset of T|oS;
      consider R being Subset of T such that
A39:  R in A and
A40:  R /\ oS = e9 by A38,TOPS_2:def 3;
      consider X1 being Subset of Y, Y1 being Subset of X such that
A41:  R = [:X1,Y1:] and
A42:  X1 is open and
A43:  Y1 is open by A36,A39;
      reconsider D2 = Y1 /\ [#]XV as Subset of XV;
      Y1 in the topology of X by A43,PRE_TOPC:def 2;
      then D2 in the topology of XV by PRE_TOPC:def 4;
      then
A44:  D2 is open by PRE_TOPC:def 2;
      [#][:Y, XV:] = [:[#]Y, [#]XV:] by BORSUK_1:def 2;
      then e9 = [:X1 /\ [#]Y, Y1 /\ [#](XV):] by A40,A41,ZFMISC_1:100;
      hence thesis by A42,A44;
    end;
A45: union A /\ oS c= union AA
    proof
      let s be object;
      assume
A46:  s in union A /\ oS;
      then s in union A by XBOOLE_0:def 4;
      then consider A1 being set such that
A47:  s in A1 and
A48:  A1 in A by TARSKI:def 4;
      s in oS by A46,XBOOLE_0:def 4;
      then
A49:  s in A1 /\ oS by A47,XBOOLE_0:def 4;
      reconsider A1 as Subset of T by A48;
      A1 /\ oS in AA by A48,TOPS_2:31;
      hence thesis by A49,TARSKI:def 4;
    end;
    union AA c= union A by TOPS_2:34;
    then union AA c= union A /\ oS by XBOOLE_1:19;
    then P = union AA by A34,A35,A45;
    then P9 is open by A37,BORSUK_1:5;
    hence thesis by PRE_TOPC:def 2;
  end;
  [#]S c= [#]T by A1,A2,ZFMISC_1:96;
  hence thesis by A3,PRE_TOPC:def 4;
end;

Lm4: for X, Y being TopSpace, Z being Subset of [:Y, X:], V being Subset of X
st Z = [:[#]Y, V:] holds the TopStruct of [:Y, X | V:] = the TopStruct of [:Y,
X:] | Z
proof
  let X, Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X;
  reconsider A = [:Y, X | V:] as SubSpace of [:Y, X:] by Th15;
  assume
A1: Z = [:[#]Y, V:];
  the carrier of A = [:the carrier of Y, the carrier of (X|V):] by
BORSUK_1:def 2
    .= Z by A1,PRE_TOPC:8
    .= the carrier of ([:Y, X:]|Z) by PRE_TOPC:8;
  then A is SubSpace of [:Y, X:] | Z & [:Y, X:] | Z is SubSpace of A by
TOPMETR:3;
  hence thesis by TSEP_1:6;
end;

theorem Th16:
  for X being non empty TopSpace, Y being compact non empty
  TopSpace, x being Point of X, Z being Subset of [:Y, X:] st Z = [:[#]Y, {x}:]
  holds Z is compact
proof
  let X be non empty TopSpace, Y be compact non empty TopSpace, x be Point of
  X, Z be Subset of [:Y, X:];
  reconsider V = {x} as non empty Subset of X;
  Y, [: Y, X | V :] are_homeomorphic by Lm3;
  then
A1: [:Y, X | V:] is compact by Th14;
  assume
A2: Z = [:[#]Y, {x}:];
  then the TopStruct of [:Y, X | V:] = the TopStruct of ([:Y, X:] | Z) by Lm4;
  hence thesis by A2,A1,COMPTS_1:3;
end;

registration
  let X be non empty TopSpace, Y be compact non empty TopSpace,
      x be Point of X;
  cluster [:Y, X|{x}:] -> compact;
coherence
proof
  Y, [: Y, X | {x} :] are_homeomorphic by Lm3;
  hence thesis by Th14;
end;
end;

theorem
  for X, Y being compact non empty TopSpace, R being Subset-Family of X
st R = { Q where Q is open Subset of X : [:[#]Y, Q:] c= union Base-Appr [#][:Y,
  X:] } holds R is open & R is Cover of [#]X
proof
  let X, Y be compact non empty TopSpace, R be Subset-Family of X;
  assume
A1: R = { Q where Q is open Subset of X : [:[#]Y, Q:] c= union Base-Appr
  [#][:Y, X:] };
  now
    let P be Subset of X;
    assume P in R;
    then ex E being open Subset of X st E = P & [:[#]Y, E:] c= union Base-Appr
    [#][:Y, X:] by A1;
    hence P is open;
  end;
  hence R is open;
  [#]X c= union R
  proof
    let k be object;
    assume k in [#]X;
    then reconsider k9 = k as Point of X;
    reconsider Z = [:[#]Y, {k9}:] as Subset of [:Y, X:];
    Z c= [#][:Y, X:];
    then Z c= union Base-Appr [#][:Y, X:] by BORSUK_1:13;
    then
A2: Base-Appr [#][:Y, X:] is Cover of Z by SETFAM_1:def 11;
    Z is compact by Th16;
    then consider G being Subset-Family of [:Y, X:] such that
A3: G c= Base-Appr [#][:Y, X:] and
A4: G is Cover of Z and
    G is finite by A2;
    set uR = union G;
    set Q = { x where x is Point of X : [:[#]Y, {x}:] c= uR };
    Q c= the carrier of X
    proof
      let k be object;
      assume k in Q;
      then ex x1 being Point of X st k = x1 & [:[#]Y, {x1}:] c= uR;
      hence thesis;
    end;
    then reconsider Q as Subset of X;
    Z c= union G by A4,SETFAM_1:def 11;
    then
A5: k9 in Q;
A6: [:[#]Y, Q:] c= union Base-Appr [#][:Y, X:]
    proof
      let z be object;
      assume z in [:[#]Y, Q:];
      then consider x1, x2 be object such that
A7:   x1 in [#]Y and
A8:   x2 in Q and
A9:  z = [x1, x2] by ZFMISC_1:def 2;
      consider x29 being Point of X such that
A10:  x29 = x2 and
A11:  [:[#]Y, {x29}:] c= uR by A8;
      x2 in {x29} by A10,TARSKI:def 1;
      then
A12:  z in [:[#]Y, {x29}:] by A7,A9,ZFMISC_1:87;
      uR c= union Base-Appr [#][:Y, X:] by A3,ZFMISC_1:77;
      then [:[#]Y, {x29}:] c= union Base-Appr [#][:Y, X:] by A11;
      hence thesis by A12;
    end;
    uR is open by A3,TOPS_2:11,19;
    then Q in the topology of X by Th12;
    then Q is open by PRE_TOPC:def 2;
    then Q in R by A1,A6;
    hence thesis by A5,TARSKI:def 4;
  end;
  hence thesis by SETFAM_1:def 11;
end;

theorem Th18:
  for X, Y being compact non empty TopSpace, R being Subset-Family
of X, F being Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open &
R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st
FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } holds R is open & R is Cover
  of X
proof
  let X, Y be compact non empty TopSpace, R be Subset-Family of X, F be
  Subset-Family of [:Y, X:];
  assume that
A1: F is Cover of [:Y, X:] and
A2: F is open and
A3: R = { Q where Q is open Subset of X : ex FQ being Subset-Family of
  [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ };
  now
    let P be Subset of X;
    assume P in R;
    then
    ex E being open Subset of X st E = P & ex FQ being Subset-Family of [:Y
    , X:] st FQ c= F & FQ is finite & [: [#]Y, E:] c= union FQ by A3;
    hence P is open;
  end;
  hence R is open;
A4: union F = [#] [:Y, X:] by A1,SETFAM_1:45;
  [#]X c= union R
  proof
    let k be object;
    assume k in [#]X;
    then reconsider k9 = k as Point of X;
    reconsider Z = [:[#]Y, {k9}:] as Subset of [:Y, X:];
    F is Cover of Z & Z is compact by A4,Th16,SETFAM_1:def 11;
    then consider G being Subset-Family of [:Y, X:] such that
A5: G c= F and
A6: G is Cover of Z and
A7: G is finite by A2;
    set uR = union G;
    set Q = { x where x is Point of X : [:[#]Y, {x}:] c= uR };
    Q c= the carrier of X
    proof
      let k be object;
      assume k in Q;
      then ex x1 being Point of X st k = x1 & [:[#]Y, {x1}:] c= uR;
      hence thesis;
    end;
    then reconsider Q as Subset of X;
    Z c= union G by A6,SETFAM_1:def 11;
    then
A8: k9 in Q;
A9: ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
    [#]Y, Q:] c= union FQ
    proof
      take G;
      [:[#]Y, Q:] c= union G
      proof
        let z be object;
        assume z in [:[#]Y, Q:];
        then consider x1, x2 be object such that
A10:    x1 in [#]Y and
A11:    x2 in Q and
A12:    z = [x1, x2] by ZFMISC_1:def 2;
        consider x29 being Point of X such that
A13:    x29 = x2 and
A14:    [:[#]Y, {x29}:] c= uR by A11;
        x2 in {x29} by A13,TARSKI:def 1;
        then z in [:[#]Y, {x29}:] by A10,A12,ZFMISC_1:87;
        hence thesis by A14;
      end;
      hence thesis by A5,A7;
    end;
    uR is open by A2,A5,TOPS_2:11,19;
    then Q in the topology of X by Th12;
    then Q is open by PRE_TOPC:def 2;
    then Q in R by A3,A9;
    hence thesis by A8,TARSKI:def 4;
  end;
  hence thesis by SETFAM_1:def 11;
end;

theorem Th19:
  for X, Y being compact non empty TopSpace, R being Subset-Family
of X, F being Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open &
R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st
  FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } holds ex C being
  Subset-Family of X st C c= R & C is finite & C is Cover of X
proof
  let X, Y be compact non empty TopSpace, R be Subset-Family of X, F be
  Subset-Family of [:Y, X:];
  assume F is Cover of [:Y, X:] & F is open & R = { Q where Q is open Subset
of X : ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y
  , Q:] c= union FQ };
  then R is open & R is Cover of X by Th18;
  then
  ex G being Subset-Family of X st G c= R & G is Cover of X & G is finite
  by COMPTS_1:def 1;
  hence thesis;
end;

theorem Th20:
  for X, Y being compact non empty TopSpace, F being Subset-Family
  of [:Y, X:] st F is Cover of [:Y, X:] & F is open ex G being Subset-Family of
  [:Y, X:] st G c= F & G is Cover of [:Y, X:] & G is finite
proof
  let X, Y be compact non empty TopSpace;
  let F be Subset-Family of [:Y, X:];
  set R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,
  X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ };
  R c= bool the carrier of X
  proof
    let s be object;
    assume s in R;
    then ex Q1 being open Subset of X st s = Q1 & ex FQ being Subset-Family of
    [:Y, X:] st FQ c= F & FQ is finite & [: [#]Y, Q1:] c= union FQ;
    hence thesis;
  end;
  then reconsider R as Subset-Family of X;
  reconsider R as Subset-Family of X;
  defpred P[object,object] means
  ex D1 being set, FQ being Subset-Family of [:Y, X:] st
    D1 = $1 & FQ c= F &
    FQ is finite & [:[#]Y, D1:] c= union FQ & $2 = FQ;
  deffunc F(set) = [:[#]Y, $1:];
  assume F is Cover of [:Y, X:] & F is open;
  then consider C being Subset-Family of X such that
A1: C c= R and
A2: C is finite and
A3: C is Cover of X by Th19;
  set CX = { F(f) where f is Subset of X : f in C };
  CX c= bool the carrier of [:Y, X:]
  proof
    let s be object;
    assume s in CX;
    then consider f1 being Subset of X such that
A4: s = F(f1) and
    f1 in C;
    [:[#]Y, f1:] c= the carrier of [:Y, X:];
    hence thesis by A4;
  end;
  then reconsider CX as Subset-Family of [:Y, X:];
  reconsider CX as Subset-Family of [:Y, X:];
A5: for e be object st e in C ex u be object st P[e,u]
  proof
    let e be object;
    assume e in C;
    then e in R by A1;
    then ex Q1 being open Subset of X st Q1 = e & ex FQ being Subset-Family of
    [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q1:] c= union FQ;
    hence thesis;
  end;
  consider t being Function such that
A6: dom t = C & for s being object st s in C holds P[s, t.s] from CLASSES1
  :sch 1(A5);
  set G = union rng t;
A7: union rng t c= F
  proof
    let k be object;
    assume k in union rng t;
    then consider K be set such that
A8: k in K and
A9: K in rng t by TARSKI:def 4;
    consider x1 be object such that
A10: x1 in dom t & K = t.x1 by A9,FUNCT_1:def 3;
    reconsider x1 as set by TARSKI:1;
    P[x1, t.x1] by A6,A10;
    then ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
    [#]Y, x1:] c= union FQ & K = FQ by A10;
    hence thesis by A8;
  end;
  G c= bool the carrier of [:Y, X:]
  proof
    let s be object;
    assume s in G;
    then s in F by A7;
    hence thesis;
  end;
  then reconsider G as Subset-Family of [:Y, X:];
  reconsider G as Subset-Family of [:Y, X:];
  take G;
  thus G c= F by A7;
  union CX = [:[#]Y, union C:]
  proof
    hereby
      let g be object;
      assume g in union CX;
      then consider GG being set such that
A11:  g in GG and
A12:  GG in CX by TARSKI:def 4;
      consider FF being Subset of X such that
A13:  GG = [:[#]Y, FF:] and
A14:  FF in C by A12;
      consider g1, g2 be object such that
A15:  g1 in [#]Y and
A16:  g2 in FF and
A17:  g = [g1, g2] by A11,A13,ZFMISC_1:def 2;
      g2 in union C by A14,A16,TARSKI:def 4;
      hence g in [:[#]Y, union C:] by A15,A17,ZFMISC_1:87;
    end;
    let g be object;
    assume g in [:[#]Y, union C:];
    then consider g1, g2 be object such that
A18: g1 in [#]Y and
A19: g2 in union C and
A20: g = [g1, g2] by ZFMISC_1:def 2;
    consider GG being set such that
A21: g2 in GG and
A22: GG in C by A19,TARSKI:def 4;
    GG in { Q where Q is open Subset of X : ex FQ being Subset-Family of
    [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } by A1,A22;
    then consider Q1 being open Subset of X such that
A23: GG = Q1 and
    ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
    [#]Y, Q1:] c= union FQ;
A24: [:[#]Y, Q1:] in CX by A22,A23;
    g in [:[#]Y, Q1:] by A18,A20,A21,A23,ZFMISC_1:87;
    hence thesis by A24,TARSKI:def 4;
  end;
  then
A25: union CX = [:[#]Y, [#]X:] by A3,SETFAM_1:45
    .= [#][:Y, X:] by BORSUK_1:def 2;
  [#][:Y, X:] c= union union rng t
  proof
    let d be object;
    assume d in [#][:Y, X:];
    then consider CC being set such that
A26: d in CC and
A27: CC in CX by A25,TARSKI:def 4;
    consider Cc being Subset of X such that
A28: CC = [:[#]Y, Cc:] and
A29: Cc in C by A27;
    Cc in R by A1,A29;
    then consider Qq being open Subset of X such that
A30: Cc = Qq and
    ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
    [#]Y, Qq:] c= union FQ;
    P[Cc, t.Cc] by A6,A29;
    then consider FQ1 being Subset-Family of [:Y, X:] such that
    FQ1 c= F and
    FQ1 is finite and
A31: [:[#]Y, Qq:] c= union FQ1 and
A32: t.Qq = FQ1 by A30;
    consider DC being set such that
A33: d in DC and
A34: DC in FQ1 by A26,A28,A30,A31,TARSKI:def 4;
    FQ1 in rng t by A6,A29,A30,A32,FUNCT_1:def 3;
    then DC in union rng t by A34,TARSKI:def 4;
    hence thesis by A33,TARSKI:def 4;
  end;
  hence G is Cover of [:Y, X:] by SETFAM_1:def 11;
A35: for X1 be set st X1 in rng t holds X1 is finite
  proof
    let X1 be set;
    assume X1 in rng t;
    then consider x1 be object such that
A36: x1 in dom t and
A37: X1 = t.x1 by FUNCT_1:def 3;
    reconsider x1 as set by TARSKI:1;
    P[x1, t.x1] by A6,A36;
    then ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
    [#]Y, x1:] c= union FQ & t.x1 = FQ;
    hence thesis by A37;
  end;
  rng t is finite by A2,A6,FINSET_1:8;
  hence thesis by A35,FINSET_1:7;
end;

Lm5: for T1, T2 be compact non empty TopSpace holds [:T1, T2:] is compact
by Th20;

registration
  let T1,T2 be compact TopSpace;
  cluster [:T1, T2:] -> compact;
  coherence
  proof
    per cases;
    suppose
      T1 is non empty & T2 is non empty;
      hence thesis by Lm5;
    end;
    suppose
      T1 is empty & T2 is empty;
      hence thesis;
    end;
    suppose
      T1 is empty & T2 is non empty;
      hence thesis;
    end;
    suppose
      T1 is non empty & T2 is empty;
      hence thesis;
    end;
  end;
end;

Lm6: for X, Y being TopSpace, XV being SubSpace of X holds [:XV, Y:] is
SubSpace of [:X, Y:]
proof
  let X, Y be TopSpace, XV be SubSpace of X;
  set S = [:XV, Y:], T = [:X, Y:];
A1: the carrier of S = [:the carrier of XV, the carrier of Y:] by
BORSUK_1:def 2;
A2: the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] & the
  carrier of XV c= the carrier of X by BORSUK_1:1,def 2;
A3: for P being Subset of S holds P in the topology of S iff ex Q being
  Subset of T st Q in the topology of T & P = Q /\ [#]S
  proof
    reconsider oS = [#]S as Subset of T by A1,A2,ZFMISC_1:96;
    let P be Subset of S;
    reconsider P9 = P as Subset of S;
    hereby
      assume P in the topology of S;
      then P9 is open by PRE_TOPC:def 2;
      then consider A being Subset-Family of S such that
A4:   P9 = union A and
A5:   for e be set st e in A ex X1 being Subset of XV, Y1 being Subset
      of Y st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
      set AA = {[:X1, Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1
being Subset of XV st Y1 = X1 /\ [#](XV) & X1 is open & Y2 is open & [:Y1, Y2:]
      in A };
      AA c= bool the carrier of T
      proof
        let a be object;
        assume a in AA;
        then
        ex Xx1 being Subset of X, Yy2 being Subset of Y st a = [: Xx1, Yy2
:] & ex Y1 being Subset of XV st Y1 = Xx1 /\ [#](XV) & Xx1 is open & Yy2 is
        open & [:Y1, Yy2:] in A;
        hence thesis;
      end;
      then reconsider AA as Subset-Family of T;
      reconsider AA as Subset-Family of T;
A6:   P c= union AA /\ [#]S
      proof
        let p be object;
        assume p in P;
        then consider A1 be set such that
A7:     p in A1 and
A8:     A1 in A by A4,TARSKI:def 4;
        reconsider A1 as Subset of S by A8;
        consider X2 being Subset of XV, Y2 being Subset of Y such that
A9:     A1 = [:X2,Y2:] and
A10:    X2 is open and
A11:    Y2 is open by A5,A8;
        X2 in the topology of XV by A10,PRE_TOPC:def 2;
        then consider Q1 being Subset of X such that
A12:    Q1 in the topology of X and
A13:    X2 = Q1 /\ [#]XV by PRE_TOPC:def 4;
        consider p1, p2 being object such that
A14:    p1 in X2 and
A15:    p2 in Y2 & p = [p1, p2] by A7,A9,ZFMISC_1:def 2;
        reconsider Q1 as Subset of X;
        set EX = [:Q1, Y2:];
        p1 in Q1 by A14,A13,XBOOLE_0:def 4;
        then
A16:    p in EX by A15,ZFMISC_1:87;
        Q1 is open by A12,PRE_TOPC:def 2;
        then
        EX in {[:Xx1, Yy2:] where Xx1 is Subset of X, Yy2 is Subset of Y:
ex Z1 being Subset of XV st Z1 = Xx1 /\ [#](XV) & Xx1 is open & Yy2 is open &
        [:Z1, Yy2:] in A } by A8,A9,A11,A13;
        then p in union AA by A16,TARSKI:def 4;
        hence thesis by A7,A8,XBOOLE_0:def 4;
      end;
      AA c= the topology of T
      proof
        let t be object;
        set A9 = { t };
        assume t in AA;
        then consider Xx1 being Subset of X, Yy2 being Subset of Y such that
A17:    t = [:Xx1, Yy2:] and
A18:    ex Y1 being Subset of XV st Y1 = Xx1 /\ [#](XV) & Xx1 is open
        & Yy2 is open & [:Y1, Yy2:] in A;
        A9 c= bool the carrier of T
        proof
          let a be object;
          assume a in A9;
          then a = t by TARSKI:def 1;
          hence thesis by A17;
        end;
        then reconsider A9 as Subset-Family of T;
A19:    A9 c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : X1
        in the topology of X & Y1 in the topology of Y }
        proof
          let x be object;
          assume x in A9;
          then
A20:      x = [:Xx1,Yy2:] by A17,TARSKI:def 1;
          Xx1 in the topology of X & Yy2 in the topology of Y by A18,
PRE_TOPC:def 2;
          hence thesis by A20;
        end;
        t = union A9;
        then t in { union As where As is Subset-Family of T : As c= { [:X1,Y1
:] where X1 is Subset of X, Y1 is Subset of Y : X1 in the topology of X & Y1 in
        the topology of Y}} by A19;
        hence thesis by BORSUK_1:def 2;
      end;
      then
A21:  union AA in the topology of T by PRE_TOPC:def 1;
      union AA /\ [#]S c= P
      proof
        let h be object;
        assume
A22:    h in union AA /\ [#]S;
        then h in union AA by XBOOLE_0:def 4;
        then consider A2 being set such that
A23:    h in A2 and
A24:    A2 in AA by TARSKI:def 4;
        consider Xx1 being Subset of X, Yy2 being Subset of Y such that
A25:    A2 = [:Xx1, Yy2:] and
A26:    ex Y1 being Subset of XV st Y1 = Xx1 /\ [#]XV & Xx1 is open &
        Yy2 is open & [:Y1, Yy2:] in A by A24;
        consider Yy1 being Subset of XV such that
A27:    Yy1 = Xx1 /\ [#]XV and
        Xx1 is open and
        Yy2 is open and
A28:    [:Yy1, Yy2:] in A by A26;
        consider p1, p2 being object such that
A29:    p1 in Xx1 and
A30:    p2 in Yy2 and
A31:    h = [p1, p2] by A23,A25,ZFMISC_1:def 2;
        p1 in the carrier of XV by A1,A22,A31,ZFMISC_1:87;
        then p1 in Xx1 /\ [#](XV) by A29,XBOOLE_0:def 4;
        then h in [:Yy1, Yy2:] by A30,A31,A27,ZFMISC_1:87;
        hence thesis by A4,A28,TARSKI:def 4;
      end;
      then P = union AA /\ [#]S by A6;
      hence
      ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S by A21;
    end;
    given Q being Subset of T such that
A32: Q in the topology of T and
A33: P = Q /\ [#]S;
    reconsider Q9 = Q as Subset of T;
    Q9 is open by A32,PRE_TOPC:def 2;
    then consider A being Subset-Family of T such that
A34: Q9 = union A and
A35: for e be set st e in A ex X1 being Subset of X, Y1 being Subset
    of Y st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
    reconsider A as Subset-Family of T;
    reconsider AA = A | oS as Subset-Family of T|oS;
    reconsider AA as Subset-Family of S by PRE_TOPC:8;
    reconsider AA as Subset-Family of S;
A36: for e be set st e in AA ex X1 being Subset of XV, Y1 being Subset of
    Y st e = [:X1,Y1:] & X1 is open & Y1 is open
    proof
      let e be set;
      assume
A37:  e in AA;
      then reconsider e9 = e as Subset of T|oS;
      consider R being Subset of T such that
A38:  R in A and
A39:  R /\ oS = e9 by A37,TOPS_2:def 3;
      consider X1 being Subset of X, Y1 being Subset of Y such that
A40:  R = [:X1,Y1:] and
A41:  X1 is open and
A42:  Y1 is open by A35,A38;
      reconsider D2 = X1 /\ [#](XV) as Subset of XV;
      X1 in the topology of X by A41,PRE_TOPC:def 2;
      then D2 in the topology of XV by PRE_TOPC:def 4;
      then
A43:  D2 is open by PRE_TOPC:def 2;
      [#][:XV, Y:] = [:[#]XV, [#]Y:] by BORSUK_1:def 2;
      then e9 = [:X1 /\ [#]XV, Y1 /\ [#]Y:] by A39,A40,ZFMISC_1:100;
      hence thesis by A42,A43;
    end;
A44: union A /\ oS c= union AA
    proof
      let s be object;
      assume
A45:  s in union A /\ oS;
      then s in union A by XBOOLE_0:def 4;
      then consider A1 being set such that
A46:  s in A1 and
A47:  A1 in A by TARSKI:def 4;
      s in oS by A45,XBOOLE_0:def 4;
      then
A48:  s in A1 /\ oS by A46,XBOOLE_0:def 4;
      reconsider A1 as Subset of T by A47;
      A1 /\ oS in AA by A47,TOPS_2:31;
      hence thesis by A48,TARSKI:def 4;
    end;
    union AA c= union A by TOPS_2:34;
    then union AA c= union A /\ oS by XBOOLE_1:19;
    then P = union AA by A33,A34,A44;
    then P9 is open by A36,BORSUK_1:5;
    hence thesis by PRE_TOPC:def 2;
  end;
  [#]S c= [#]T by A1,A2,ZFMISC_1:96;
  hence thesis by A3,PRE_TOPC:def 4;
end;

theorem Th21:
  for X, Y being TopSpace, XV being SubSpace of X, YV being
  SubSpace of Y holds [:XV, YV:] is SubSpace of [:X, Y:]
proof
  let X, Y be TopSpace, XV be SubSpace of X, YV be SubSpace of Y;
  [:XV, Y:] is SubSpace of [:X, Y:] & [:XV, YV:] is SubSpace of [:XV, Y:]
  by Lm6,Th15;
  hence thesis by TSEP_1:7;
end;

theorem Th22:
  for X, Y being TopSpace, Z being Subset of [:Y, X:], V being
Subset of X, W being Subset of Y st Z = [:W, V:] holds the TopStruct of [:Y | W
  , X | V:] = the TopStruct of [:Y, X:] | Z
proof
  let X, Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X, W be Subset
  of Y;
  reconsider A = [:Y | W, X | V:] as SubSpace of [:Y, X:] by Th21;
  assume
A1: Z = [:W, V:];
  the carrier of A = [:the carrier of (Y|W), the carrier of (X|V):] by
BORSUK_1:def 2
    .= [:the carrier of (Y|W), V:] by PRE_TOPC:8
    .= Z by A1,PRE_TOPC:8
    .= the carrier of ([:Y, X:]|Z) by PRE_TOPC:8;
  then A is SubSpace of [:Y, X:] | Z & [:Y, X:] | Z is SubSpace of A by
TOPMETR:3;
  hence thesis by TSEP_1:6;
end;

registration
  let T be TopSpace;
  cluster empty for Subset of T;
  existence
  proof
    take {}T;
    thus thesis;
  end;
end;

registration
  let T be TopSpace, P be compact Subset of T;
  cluster T | P -> compact;
  coherence
  proof
    per cases;
    suppose
      P is non empty;
      hence thesis by COMPTS_1:3;
    end;
    suppose
      P is empty;
      hence thesis;
    end;
  end;
end;

theorem
  for T1, T2 being TopSpace, S1 being Subset of T1, S2 being Subset of
T2 st S1 is compact & S2 is compact holds [:S1, S2:] is compact Subset of [:T1,
  T2:]
proof
  let T1, T2 be TopSpace, S1 be Subset of T1, S2 be Subset of T2;
  assume that
A1: S1 is compact and
A2: S2 is compact;
  per cases;
  suppose
A3: S1 is non empty & S2 is non empty;
    then (ex x be object st x in S1 )& ex y be object st y in S2;
    then reconsider T1, T2 as non empty TopSpace;
    reconsider S2 as compact non empty Subset of T2 by A2,A3;
    reconsider S1 as compact non empty Subset of T1 by A1,A3;
    reconsider X = [:S1, S2:] as Subset of [:T1, T2:];
    the TopStruct of [:T1|S1, T2|S2:] = the TopStruct of ([:T1, T2:] | X)
    by Th22;
    hence thesis by COMPTS_1:3;
  end;
  suppose
    S1 is empty & S2 is non empty;
    then reconsider S1 as empty Subset of T1;
    [:S1, S2:] = {}([:T1, T2:]);
    hence thesis;
  end;
  suppose
    S1 is non empty & S2 is empty;
    then reconsider S2 as empty Subset of T2;
    [:S1, S2:] = {}([:T1, T2:]);
    hence thesis;
  end;
  suppose
    S1 is empty & S2 is empty;
    then reconsider S2 as empty Subset of T2;
    [:S1, S2:] = {}([:T1, T2:]);
    hence thesis;
  end;
end;