YELLOW16

:: Retracts and Inheritance
::  by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999-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 RELAT_1, TARSKI, XBOOLE_0, ORDERS_2, YELLOW_0, FUNCT_1, STRUCT_0,
      XXREAL_0, SUBSET_1, CAT_1, RELAT_2, WAYBEL_0, SEQM_3, FUNCOP_1, ORDINAL2,
      BINOP_1, GROUP_6, EQREL_1, FUNCT_3, BORSUK_1, WAYBEL_1, WELLORD1,
      REWRITE1, YELLOW_1, WAYBEL_3, NEWTON, CARD_3, PBOOLE, LATTICE3, FUNCT_4,
      RLVECT_2, ZFMISC_1, LATTICES, PRE_TOPC, RCOMP_1, WAYBEL18, CARD_1,
      YELLOW_9, T_0TOPSP, TOPS_2, YELLOW16, FUNCT_2;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, ORDINAL1, NUMBERS, FUNCT_7,
      FUNCOP_1, STRUCT_0, CARD_3, PRALG_1, FUNCT_4, WELLORD1, ORDERS_2,
      LATTICE3, PRE_TOPC, TOPS_2, T_0TOPSP, BORSUK_1, QUANTAL1, YELLOW_0,
      WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3, WAYBEL18;
 constructors TOLER_1, FUNCT_7, TOPS_2, BORSUK_1, T_0TOPSP, MONOID_0, QUANTAL1,
      ORDERS_3, YELLOW_9, WAYBEL18, WAYBEL20, FUNCT_4;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, STRUCT_0,
      PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, MONOID_0, BORSUK_2,
      WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, WAYBEL10, WAYBEL17,
      WAYBEL18, RELAT_1;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions TARSKI, RELAT_1, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_1,
      YELLOW_2, WAYBEL_1, WAYBEL_3, T_0TOPSP, WAYBEL25, XBOOLE_0;
 equalities ORDINAL1, YELLOW_1, YELLOW_2, WAYBEL_1, STRUCT_0;
 expansions TARSKI, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_2, WAYBEL_1,
      T_0TOPSP;
 theorems YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC, BORSUK_1,
      ORDERS_2, YELLOW12, RELAT_1, FUNCT_2, FUNCT_1, ENUMSET1, WAYBEL_3,
      FUNCOP_1, CARD_3, TARSKI, ZFMISC_1, WELLORD1, QUANTAL1, FUNCT_4,
      YELLOW_9, WAYBEL20, FUNCT_7, TOPS_2, FUNCT_3, WAYBEL10, WAYBEL15,
      YELLOW_6, PRALG_1, WAYBEL18, WAYBEL13, WAYBEL21, XBOOLE_0, XBOOLE_1,
      PARTFUN1, CARD_1;
 schemes PBOOLE;

begin :: Poset retracts

::$CT

theorem
  for X being set, L being non empty RelStr, S being non empty SubRelStr
of L for f,g being Function of X, the carrier of S for f9,g9 being Function of
  X, the carrier of L st f9 = f & g9 = g & f <= g holds f9 <= g9
proof
  let X be set, L be non empty RelStr, S be non empty SubRelStr of L;
  let f,g be Function of X, the carrier of S;
  let f9,g9 be Function of X, the carrier of L such that
A1: f9 = f and
A2: g9 = g and
A3: f <= g;
  let x be set;
  assume
A4: x in X;
  then reconsider a = f.x, b = g.x as Element of S by FUNCT_2:5;
  reconsider a9 = a, b9 = b as Element of L by YELLOW_0:58;
  take a9, b9;
  thus a9 = f9.x & b9 = g9.x by A1,A2;
  ex a,b being Element of S st a = f.x & b = g.x & a <= b by A3,A4;
  hence thesis by YELLOW_0:59;
end;

theorem
  for X being set, L being non empty RelStr for S being full non empty
  SubRelStr of L for f,g being Function of X, the carrier of S for f9,g9 being
  Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds f <= g
proof
  let X be set, L be non empty RelStr;
  let S be full non empty SubRelStr of L;
  let f,g be Function of X, the carrier of S;
  let f9,g9 be Function of X, the carrier of L such that
A1: f9 = f and
A2: g9 = g and
A3: f9 <= g9;
  let x be set;
  assume
A4: x in X;
  then reconsider a = f.x, b = g.x as Element of S by FUNCT_2:5;
  take a, b;
  thus a = f.x & b = g.x;
  ex a9,b9 being Element of L st a9 = a & b9 = b & a9 <= b9 by A1,A2,A3,A4;
  hence thesis by YELLOW_0:60;
end;

registration
  let S be non empty RelStr;
  let T be non empty reflexive antisymmetric RelStr;
  cluster directed-sups-preserving monotone for Function of S,T;
  existence
  proof
    set x = the Element of T;
    take f = S --> x;
    thus f is directed-sups-preserving
    proof
      let X be Subset of S;
      assume
A1:   X is non empty directed;
A2:   f.:X = {x}
      proof
        set a = the Element of X;
        thus f.:X c= {x} by FUNCOP_1:81;
A3:     dom f = the carrier of S;
A4:     a in X by A1;
        then f.a = x by FUNCOP_1:7;
        then x in f.:X by A4,A3,FUNCT_1:def 6;
        hence thesis by ZFMISC_1:31;
      end;
      assume ex_sup_of X,S;
      thus ex_sup_of f.:X, T by A2,YELLOW_0:38;
      thus sup (f.:X) = x by A2,YELLOW_0:39
        .= f.sup X;
    end;
    let a,b be Element of S;
A5: x <= x;
    thus thesis by A5;
  end;
end;

theorem
  for f,g being Function st f is idempotent & rng g c= rng f & rng g c=
  dom f holds f*g = g
proof
  let f,g be Function;
  assume f is idempotent;
  then
A1: f*f = f by QUANTAL1:def 9;
  assume
A2: rng g c= rng f;
A3: now
    let x be object;
    assume
A4: x in dom g;
    then g.x in rng g by FUNCT_1:def 3;
    then
A5: ex a being object st a in dom f & g.x = f.a by A2,FUNCT_1:def 3;
    (f*g).x = f.(g.x) by A4,FUNCT_1:13;
    hence (f*g).x = g.x by A1,A5,FUNCT_1:13;
  end;
  assume rng g c= dom f;
  then dom (f*g) = dom g by RELAT_1:27;
  hence thesis by A3,FUNCT_1:2;
end;

registration
  let S be 1-sorted;
  cluster idempotent for Function of S,S;
  existence
  proof
    take f = id S;
    f*f = f by FUNCT_2:17;
    hence thesis by QUANTAL1:def 9;
  end;
end;

theorem Th4:
  for L being up-complete non empty Poset for S being
directed-sups-inheriting full non empty SubRelStr of L holds S is up-complete
proof
  let L be up-complete non empty Poset;
  let S be directed-sups-inheriting full non empty SubRelStr of L;
  now
    let X be non empty directed Subset of S;
    reconsider Y = X as non empty directed Subset of L by YELLOW_2:7;
    ex_sup_of Y,L by WAYBEL_0:75;
    hence ex_sup_of X,S by WAYBEL_0:7;
  end;
  hence thesis by WAYBEL_0:75;
end;

theorem Th5:
  for L being up-complete non empty Poset for f being Function of
  L, L st f is idempotent directed-sups-preserving holds Image f is
  directed-sups-inheriting
proof
  let L be up-complete non empty Poset;
  let f be Function of L, L;
  set S = subrelstr(rng f);
  set a = the Element of L;
  reconsider S9 = S as non empty full SubRelStr of L;
  assume
A1: f is idempotent directed-sups-preserving;
  S is directed-sups-inheriting
  proof
    let X be directed Subset of S;
    X c= the carrier of S;
    then
A2: X c= rng f by YELLOW_0:def 15;
    assume X <> {};
    then X is non empty directed Subset of S9;
    then reconsider X9= X as non empty directed Subset of L by YELLOW_2:7;
    assume
A3: ex_sup_of X,L;
    f preserves_sup_of X9 by A1;
    then sup(f.:X9) = f.sup X9 by A3;
    then sup X9 = f.sup X9 by A1,A2,YELLOW_2:20;
    then "\/"(X, L) in rng f by FUNCT_2:4;
    hence thesis by YELLOW_0:def 15;
  end;
  hence thesis;
end;

theorem Th6:
  for T being non empty RelStr, S being non empty SubRelStr of T
  for f being Function of T,S holds f*incl(S,T) = id S implies f is idempotent
  Function of T, T
proof
  let T be non empty RelStr, S be non empty SubRelStr of T;
  let f be Function of T,S;
  assume
A1: f*incl(S, T) = id S;
A2: the carrier of S c= the carrier of T by YELLOW_0:def 13;
  then incl(S, T) = id the carrier of S by YELLOW_9:def 1;
  then incl(S, T)*f = f by FUNCT_2:17;
  then
A3: f*f = (id the carrier of S)*f by A1,RELAT_1:36
    .= f by FUNCT_2:17;
A4: dom f = the carrier of T by FUNCT_2:def 1;
  f is onto by A1,FUNCT_2:23;
  then rng f = the carrier of S by FUNCT_2:def 3;
  hence thesis by A2,A3,A4,FUNCT_2:2,QUANTAL1:def 9;
end;

definition
  let S,T be non empty Poset;
  let f be Function;
  pred f is_a_retraction_of T,S means

  f is directed-sups-preserving
  Function of T,S & f|the carrier of S = id S & S is directed-sups-inheriting
  full SubRelStr of T;
  pred f is_an_UPS_retraction_of T,S means

  f is
directed-sups-preserving Function of T,S & ex g being directed-sups-preserving
  Function of S,T st f*g = id S;
end;

definition
  let S,T be non empty Poset;
  pred S is_a_retract_of T means

  ex f being Function of T,S st f is_a_retraction_of T,S;
  pred S is_an_UPS_retract_of T means

  ex f being Function of T,S st f is_an_UPS_retraction_of T,S;
end;

theorem Th7:
  for S,T being non empty Poset, f being Function st f
  is_a_retraction_of T,S holds f*incl(S,T) = id S
proof
  let S,T be non empty Poset, f be Function such that
  f is directed-sups-preserving Function of T,S and
A1: f|the carrier of S = id S and
A2: S is directed-sups-inheriting full SubRelStr of T;
  the carrier of S c= the carrier of T by A2,YELLOW_0:def 13;
  hence f*incl(S, T) = f*id the carrier of S by YELLOW_9:def 1
    .= id S by A1,RELAT_1:65;
end;

theorem Th8:
  for S being non empty Poset, T being up-complete non empty
  Poset for f being Function st f is_a_retraction_of T,S holds f
  is_an_UPS_retraction_of T,S
proof
  let S be non empty Poset;
  let T be up-complete non empty Poset, f be Function;
  assume
A1: f is_a_retraction_of T,S;
  hence f is directed-sups-preserving Function of T,S;
  S is directed-sups-inheriting full SubRelStr of T by A1;
  then reconsider
  g = incl(S,T) as directed-sups-preserving Function of S,T by WAYBEL21:10;
  take g;
  thus thesis by A1,Th7;
end;

theorem Th9:
  for S,T being non empty Poset, f being Function st f
  is_a_retraction_of T,S holds rng f = the carrier of S
proof
  let S,T be non empty Poset, f be Function;
  assume
A1: f is_a_retraction_of T,S;
  then reconsider f as Function of T,S;
  f*incl(S,T) = id S by A1,Th7;
  then f is onto by FUNCT_2:23;
  hence thesis by FUNCT_2:def 3;
end;

theorem Th10:
  for S,T being non empty Poset, f being Function st f
  is_an_UPS_retraction_of T,S holds rng f = the carrier of S
proof
  let S,T be non empty Poset, f be Function;
  assume that
A1: f is directed-sups-preserving Function of T,S and
A2: ex g being directed-sups-preserving Function of S,T st f*g = id S;
   reconsider f as Function of T,S by A1;
   f is onto by A2,FUNCT_2:23;
  hence thesis by FUNCT_2:def 3;
end;

theorem Th11:
  for S,T being non empty Poset, f being Function st f
  is_a_retraction_of T,S holds f is idempotent Function of T,T
proof
  let S,T be non empty Poset, f be Function;
  assume
A1: f is_a_retraction_of T,S;
  then
A2: f is Function of T,S;
A3: S is SubRelStr of T by A1;
  f*incl(S,T) = id S by A1,Th7;
  hence thesis by A2,A3,Th6;
end;

theorem Th12:
  for T,S being non empty Poset, f being Function of T,T st f
  is_a_retraction_of T,S holds Image f = the RelStr of S
proof
  let T,S be non empty Poset, f be Function of T,T;
A1: the carrier of Image f = rng f by YELLOW_0:def 15;
  assume
A2: f is_a_retraction_of T,S;
  thus thesis by A2,A1,Th9,YELLOW_0:57;
end;

theorem Th13:
  for T being up-complete non empty Poset for S being non empty
  Poset, f being Function of T,T st f is_a_retraction_of T,S holds f is
  directed-sups-preserving projection
proof
  let T be up-complete non empty Poset;
  let S be non empty Poset, f be Function of T,T;
  assume
A1: f is_a_retraction_of T,S;
  then reconsider g = f as directed-sups-preserving Function of T,S;
  f is idempotent by A1,Th11;
  then
A2: f = f*f by QUANTAL1:def 9
    .= (f|rng f)*f by FUNCT_4:2
    .= (f|the carrier of S)*f by A1,Th8,Th10
    .= (id S)*f by A1
    .= (id the carrier of S)*g;
A3: S is full directed-sups-inheriting non empty SubRelStr of T by A1;
  then
A4: incl(S,T) is directed-sups-preserving by WAYBEL21:10;
  the carrier of S c= the carrier of T by A3,YELLOW_0:def 13;
  then
A5: incl(S,T) = id the carrier of S by YELLOW_9:def 1;
  hence f is directed-sups-preserving by A2,A4,WAYBEL20:28;
  f is directed-sups-preserving idempotent Function of T,T by A1,A2,A4,A5,Th11,
WAYBEL20:28;
  hence thesis;
end;

theorem Th14:
  for S,T being non empty reflexive transitive RelStr for f being
  Function of S,T holds f is isomorphic iff f is monotone & ex g being monotone
  Function of T,S st f*g = id T & g*f = id S
proof
  let S,T be non empty reflexive transitive RelStr, f be Function of S,T;
  hereby
    assume
A1: f is isomorphic;
    hence f is monotone;
    consider g being Function of T,S such that
A2: g = f qua Function" and
A3: g is monotone by A1,WAYBEL_0:def 38;
    reconsider g as monotone Function of T,S by A3;
    take g;
    rng f = the carrier of T by A1,WAYBEL_0:66;
    hence f*g = id T & g*f = id S by A1,A2,FUNCT_2:29;
  end;
  assume
A4: f is monotone;
  given g being monotone Function of T,S such that
A5: f*g = id T and
A6: g*f = id S;
A7: f is one-to-one by A6,FUNCT_2:23;
  f is onto by A5,FUNCT_2:23;
  then rng f = the carrier of T by FUNCT_2:def 3;
  then g = f qua Function" by A6,A7,FUNCT_2:30;
  hence thesis by A4,A7,WAYBEL_0:def 38;
end;

theorem Th15:
  for S,T being non empty Poset holds S,T are_isomorphic iff ex f
being monotone Function of S,T, g being monotone Function of T,S st f*g = id T
  & g*f = id S
proof
  let S,T be non empty Poset;
  hereby
    assume S,T are_isomorphic;
    then consider f being Function of S,T such that
A1: f is isomorphic;
    reconsider f as monotone Function of S,T by A1;
    consider g being Function of T,S such that
A2: g = f qua Function" and
A3: g is monotone by A1,WAYBEL_0:def 38;
    take f;
    reconsider g as monotone Function of T,S by A3;
    take g;
    rng f = the carrier of T by A1,WAYBEL_0:66;
    hence f*g = id T & g*f = id S by A1,A2,FUNCT_2:29;
  end;
  given f being monotone Function of S,T, g being monotone Function of T,S
  such that
A4: f*g = id T and
A5: g*f = id S;
  take f;
A6: f is one-to-one by A5,FUNCT_2:23;
  f is onto by A4,FUNCT_2:23;
  then rng f = the carrier of T by FUNCT_2:def 3;
  then g = f qua Function" by A5,A6,FUNCT_2:30;
  hence thesis by A6,WAYBEL_0:def 38;
end;

theorem
  for S,T being up-complete non empty Poset st S,T are_isomorphic
  holds S is_an_UPS_retract_of T & T is_an_UPS_retract_of S
proof
  let S,T be up-complete non empty Poset;
  assume S,T are_isomorphic;
  then consider
  f be monotone Function of S,T, g be monotone Function of T,S such
  that
A1: f*g = id T and
A2: g*f = id S by Th15;
  g is isomorphic by A1,A2,Th14;
  then
A3: g is sups-preserving by WAYBEL13:20;
  f is isomorphic by A1,A2,Th14;
  then
A4: f is sups-preserving by WAYBEL13:20;
  then
A5: f is_an_UPS_retraction_of S,T by A1,A3;
  g is_an_UPS_retraction_of T,S by A2,A4,A3;
  hence thesis by A5;
end;

theorem Th17:
  for T,S being non empty Poset for f being monotone Function of T
  ,S, g being monotone Function of S,T st f*g = id S ex h being projection
Function of T,T st h = g*f & h|the carrier of Image h = id Image h & S, Image h
  are_isomorphic
proof
  let T,S be non empty Poset;
  let f be monotone Function of T,S, g be monotone Function of S,T such that
A1: f*g = id S;
  set h = g*f;
  h*h = h*g*f by RELAT_1:36
    .= g*(id S)*f by A1,RELAT_1:36
    .= h by FUNCT_2:17;
  then h is idempotent monotone Function of T,T by QUANTAL1:def 9,YELLOW_2:12;
  then reconsider h as projection Function of T,T by WAYBEL_1:def 13;
A2: dom g = the carrier of S by FUNCT_2:def 1;
    f is onto by A1,FUNCT_2:23;
    then
A3: rng f = the carrier of S by FUNCT_2:def 3;
  then reconsider gg = corestr g as Function of S, Image h by A2,RELAT_1:28;
A4: gg = g by WAYBEL_1:30;
A5: now
    let x,y be Element of S;
    x <= y implies g.x <= g.y & gg.x in the carrier of Image h by
WAYBEL_1:def 2;
    hence x <= y implies gg.x <= gg.y by A4,YELLOW_0:60;
    (id S).x = x;
    then
A6: x = f.(g.x) by A1,FUNCT_2:15;
    (id S).y = y;
    then
A7: y = f.(g.y) by A1,FUNCT_2:15;
    assume gg.x <= gg.y;
    then g.x <= g.y by A4,YELLOW_0:59;
    hence x <= y by A6,A7,WAYBEL_1:def 2;
  end;
  rng h = rng g by A3,A2,RELAT_1:28;
  then
A8: rng gg = the carrier of Image h by A4,YELLOW_0:def 15;
  take h;
  thus h = g*f;
  thus h|the carrier of Image h = h*(inclusion h) by RELAT_1:65
    .= (corestr h)*(inclusion h) by WAYBEL_1:30
    .= id Image h by WAYBEL_1:33;
  take gg;
  gg is one-to-one by A1,A4,FUNCT_2:23;
  hence thesis by A8,A5,WAYBEL_0:66;
end;

theorem Th18:
  for T being up-complete non empty Poset, S being non empty
  Poset for f being Function st f is_an_UPS_retraction_of T,S ex h being
directed-sups-preserving projection Function of T,T st h is_a_retraction_of T,
  Image h & S, Image h are_isomorphic
proof
  let T be up-complete non empty Poset;
  let S be non empty Poset, f be Function such that
A1: f is directed-sups-preserving Function of T,S;
  given g being directed-sups-preserving Function of S,T such that
A2: f*g = id S;
  reconsider f as directed-sups-preserving Function of T,S by A1;
  consider h being projection Function of T,T such that
A3: h = g*f and
A4: h|the carrier of Image h = id Image h and
A5: S, Image h are_isomorphic by A2,Th17;
  reconsider h as directed-sups-preserving projection Function of T,T by A3,
WAYBEL20:28;
  take h;
  reconsider R = Image h as non empty Poset;
  h = corestr h by WAYBEL_1:30;
  then
A6: h is directed-sups-preserving Function of T, R by WAYBEL20:22;
  R is directed-sups-inheriting full SubRelStr of T by Th5;
  hence h is_a_retraction_of T, Image h by A4,A6;
  thus thesis by A5;
end;

theorem Th19:
  for L being up-complete non empty Poset for S being non empty
  Poset st S is_a_retract_of L holds S is up-complete
proof
  let L be up-complete non empty Poset;
  let S be non empty Poset;
  given f being Function of L,S such that
A1: f is_a_retraction_of L,S;
  S is full directed-sups-inheriting non empty SubRelStr of L by A1;
  hence thesis by Th4;
end;

theorem Th20:
  for L being complete non empty Poset for S being non empty
  Poset st S is_a_retract_of L holds S is complete
proof
  let L be complete non empty Poset;
  let S be non empty Poset;
  given f being Function of L, S such that
A1: f is_a_retraction_of L,S;
  reconsider f as directed-sups-preserving projection Function of L,L by A1
,Th11,Th13;
A2: Image f is complete by YELLOW_2:35;
  the RelStr of S = Image f by A1,Th12;
  hence thesis by A2,YELLOW_0:3;
end;

theorem Th21:
  for L being continuous complete LATTICE for S being non empty
  Poset st S is_a_retract_of L holds S is continuous
proof
  let L be continuous complete LATTICE;
  let S be non empty Poset;
  given f being Function of L,S such that
A1: f is_a_retraction_of L,S;
  reconsider g = f as directed-sups-preserving projection Function of L,L by A1
,Th11,Th13;
A2: Image g is continuous LATTICE by WAYBEL15:15;
  Image g = the RelStr of S by A1,Th12;
  hence thesis by A2,YELLOW12:15;
end;

theorem
  for L being up-complete non empty Poset for S being non empty Poset
  st S is_an_UPS_retract_of L holds S is up-complete
proof
  let L be up-complete non empty Poset;
  let S be non empty Poset;
  given f being Function of L,S such that
A1: f is_an_UPS_retraction_of L,S;
  consider h being directed-sups-preserving projection Function of L,L such
  that
A2: h is_a_retraction_of L, Image h and
A3: S, Image h are_isomorphic by A1,Th18;
  Image h is_a_retract_of L by A2;
  then Image h is up-complete by Th19;
  hence thesis by A3,WAYBEL13:30,WAYBEL_1:6;
end;

theorem
  for L being complete non empty Poset for S being non empty Poset st
  S is_an_UPS_retract_of L holds S is complete
proof
  let L be complete non empty Poset, S be non empty Poset;
  given f being Function of L, S such that
A1: f is_an_UPS_retraction_of L,S;
  consider h being directed-sups-preserving projection Function of L,L such
  that
A2: h is_a_retraction_of L, Image h and
A3: S, Image h are_isomorphic by A1,Th18;
  Image h is_a_retract_of L by A2;
  then Image h is complete by Th20;
  hence thesis by A3,WAYBEL20:18,WAYBEL_1:6;
end;

theorem
  for L being continuous complete LATTICE for S being non empty Poset st
  S is_an_UPS_retract_of L holds S is continuous
proof
  let L be continuous complete LATTICE;
  let S be non empty Poset;
  given f being Function of L,S such that
A1: f is_an_UPS_retraction_of L,S;
  consider h being directed-sups-preserving projection Function of L,L such
  that
A2: h is_a_retraction_of L, Image h and
A3: S, Image h are_isomorphic by A1,Th18;
  Image h is_a_retract_of L by A2;
  then Image h is continuous by Th21;
  hence thesis by A3,WAYBEL15:9,WAYBEL_1:6;
end;

theorem Th25:
  for L being RelStr for S being full SubRelStr of L for R being
  SubRelStr of S holds R is full iff R is full SubRelStr of L
proof
  let L be RelStr, S be full SubRelStr of L, R be SubRelStr of S;
  reconsider R9 = R as SubRelStr of L by YELLOW_6:7;
A1: the carrier of R c= the carrier of S by YELLOW_0:def 13;
  hereby
    assume R is full;
    then the InternalRel of R = (the InternalRel of S)|_2 the carrier of R
      .= ((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R by
YELLOW_0:def 14
      .= (the InternalRel of L)|_2 the carrier of R9 by A1,WELLORD1:22;
    hence R is full SubRelStr of L by YELLOW_0:def 14;
  end;
  assume
A2: R is full SubRelStr of L;
  ((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R = (the
  InternalRel of L)|_2 the carrier of R by A1,WELLORD1:22
    .= the InternalRel of R by A2,YELLOW_0:def 14;
  hence the InternalRel of R = (the InternalRel of S)|_2 the carrier of R by
YELLOW_0:def 14;
end;

theorem
  for L being non empty transitive RelStr for S being
  directed-sups-inheriting non empty full SubRelStr of L for R being
  directed-sups-inheriting non empty SubRelStr of S holds R is
  directed-sups-inheriting SubRelStr of L
proof
  let L be non empty transitive RelStr;
  let S be directed-sups-inheriting non empty full SubRelStr of L;
  let R be directed-sups-inheriting non empty SubRelStr of S;
  reconsider T = R as SubRelStr of L by YELLOW_6:7;
  T is directed-sups-inheriting
  proof
    let X be directed Subset of T;
    reconsider Y = X as directed Subset of S by YELLOW_2:7;
    assume
A1: X <> {};
    assume
A2: ex_sup_of X,L;
    then
A3: ex_sup_of Y, S by A1,WAYBEL_0:7;
    sup Y = "\/"(X,L) by A1,A2,WAYBEL_0:7;
    hence thesis by A1,A3,WAYBEL_0:def 4;
  end;
  hence thesis;
end;

theorem
  for L being up-complete non empty Poset for S1,S2 being
directed-sups-inheriting full non empty SubRelStr of L st S1 is SubRelStr of S2
  holds S1 is directed-sups-inheriting full SubRelStr of S2
proof
  let L be up-complete non empty Poset;
  let S1,S2 be directed-sups-inheriting full non empty SubRelStr of L;
  assume S1 is SubRelStr of S2;
  then reconsider S = S1 as SubRelStr of S2;
  S is directed-sups-inheriting
  proof
    let X be directed Subset of S;
    assume X <> {};
    then reconsider Y1 = X as non empty directed Subset of S1;
    reconsider Y2 = Y1 as non empty directed Subset of S2 by YELLOW_2:7;
    reconsider Y = Y1 as non empty directed Subset of L by YELLOW_2:7;
A1: ex_sup_of Y, L by WAYBEL_0:75;
    then
A2: sup Y = sup Y1 by WAYBEL_0:7;
    sup Y2 = sup Y by A1,WAYBEL_0:7;
    hence thesis by A2;
  end;
  hence thesis by Th25;
end;

begin :: Products

definition
  let R be Relation;
  attr R is Poset-yielding means
  :Def5:
  for x being set st x in rng R holds x is Poset;
end;

registration
  cluster Poset-yielding -> RelStr-yielding reflexive-yielding for Relation;
  coherence
  proof
    let R be Relation;
    assume
A1: for x being set st x in rng R holds x is Poset;
    hence for x being set st x in rng R holds x is RelStr;
    thus for S being RelStr st S in rng R holds S is reflexive by A1;
  end;
end;

definition
  let X be non empty set;
  let L be non empty RelStr;
  let i be Element of X;
  let Y be Subset of L|^X;
  redefine func pi(Y,i) -> Subset of L;  :: redefines pi (CARD_3, definition)
  coherence
  proof
    reconsider Y9 = Y as Subset of product (X --> L);
    pi(Y9,i) is Subset of (X --> L).i;
    hence thesis;
  end;
end;

registration
  let X be set;
  let S be Poset;
  cluster X --> S -> Poset-yielding;
  coherence
  proof
    let x be set;
    assume x in rng (X --> S);
    hence thesis by TARSKI:def 1;
  end;
end;

registration
  let I be set;
  cluster Poset-yielding non-Empty for ManySortedSet of I;
  existence
  proof
    set P = the non empty Poset;
    take I --> P;
    thus thesis;
  end;
end;

registration
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  cluster product J -> transitive antisymmetric;
  coherence
  proof
A1: now
      let i be Element of I;
      dom J = I by PARTFUN1:def 2;
      then J.i in rng J by FUNCT_1:def 3;
      hence J.i is Poset by Def5;
    end;
    then for i being Element of I holds J.i is transitive;
    hence product J is transitive by WAYBEL_3:29;
    for i being Element of I holds J.i is antisymmetric by A1;
    hence thesis by WAYBEL_3:30;
  end;
end;

definition
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let i be Element of I;
  redefine func J.i -> non empty Poset;  :: redefines . (FUNCT_1, definition)
  coherence
  proof
    dom J = I by PARTFUN1:def 2;
    then J.i in rng J by FUNCT_1:def 3;
    hence thesis by Def5;
  end;
end;

Lm1: now
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let X be Subset of product J;
  deffunc F(Element of I) = sup pi(X,$1);
  consider f being ManySortedSet of I such that
A1: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A2: now
    let i be Element of I;
    f.i = sup pi(X,i) by A1;
    hence f.i is Element of J.i;
  end;
  dom f = I by PARTFUN1:def 2;
  then reconsider f as Element of product J by A2,WAYBEL_3:27;
  assume
A3: for i being Element of I holds ex_sup_of pi(X,i), J.i;
  take f;
  thus for i being Element of I holds f.i = sup pi(X,i) by A1;
  thus f is_>=_than X
  proof
    let x be Element of product J such that
A4: x in X;
    now
      let i be Element of I;
A5:   f.i = sup pi(X,i) by A1;
A6:   x.i in pi(X,i) by A4,CARD_3:def 6;
      ex_sup_of pi(X,i), J.i by A3;
      then f.i is_>=_than pi(X,i) by A5,YELLOW_0:30;
      hence x.i <= f.i by A6;
    end;
    hence thesis by WAYBEL_3:28;
  end;
  let g be Element of product J;
  assume
A7: X is_<=_than g;
  now
    let i be Element of I;
A8: ex_sup_of pi(X,i), J.i by A3;
A9: g.i is_>=_than pi(X,i)
    proof
      let a be Element of J.i;
      assume a in pi(X,i);
      then consider h being Function such that
A10:  h in X and
A11:  a = h.i by CARD_3:def 6;
      reconsider h as Element of product J by A10;
      h <= g by A7,A10;
      hence a <= g.i by A11,WAYBEL_3:28;
    end;
    f.i = sup pi(X,i) by A1;
    hence f.i <= g.i by A8,A9,YELLOW_0:30;
  end;
  hence f <= g by WAYBEL_3:28;
end;

Lm2: now
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let X be Subset of product J;
  deffunc F(Element of I) = inf pi(X,$1);
  consider f being ManySortedSet of I such that
A1: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A2: now
    let i be Element of I;
    f.i = inf pi(X,i) by A1;
    hence f.i is Element of J.i;
  end;
  dom f = I by PARTFUN1:def 2;
  then reconsider f as Element of product J by A2,WAYBEL_3:27;
  assume
A3: for i being Element of I holds ex_inf_of pi(X,i), J.i;
  take f;
  thus for i being Element of I holds f.i = inf pi(X,i) by A1;
  thus f is_<=_than X
  proof
    let x be Element of product J such that
A4: x in X;
    now
      let i be Element of I;
A5:   f.i = inf pi(X,i) by A1;
A6:   x.i in pi(X,i) by A4,CARD_3:def 6;
      ex_inf_of pi(X,i), J.i by A3;
      then f.i is_<=_than pi(X,i) by A5,YELLOW_0:31;
      hence x.i >= f.i by A6;
    end;
    hence thesis by WAYBEL_3:28;
  end;
  let g be Element of product J;
  assume
A7: X is_>=_than g;
  now
    let i be Element of I;
A8: ex_inf_of pi(X,i), J.i by A3;
A9: g.i is_<=_than pi(X,i)
    proof
      let a be Element of J.i;
      assume a in pi(X,i);
      then consider h being Function such that
A10:  h in X and
A11:  a = h.i by CARD_3:def 6;
      reconsider h as Element of product J by A10;
      h >= g by A7,A10;
      hence a >= g.i by A11,WAYBEL_3:28;
    end;
    f.i = inf pi(X,i) by A1;
    hence f.i >= g.i by A8,A9,YELLOW_0:31;
  end;
  hence f >= g by WAYBEL_3:28;
end;

theorem Th28:
  for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for f being Element of product J, X being Subset of product
J holds f is_>=_than X iff for i being Element of I holds f.i is_>=_than pi(X,i
  )
proof
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let f be Element of product J, X be Subset of product J;
  hereby
    assume
A1: f is_>=_than X;
    let i be Element of I;
    thus f.i is_>=_than pi(X, i)
    proof
      let x be Element of J.i;
      assume x in pi(X, i);
      then consider g being Function such that
A2:   g in X and
A3:   x = g.i by CARD_3:def 6;
      reconsider g as Element of product J by A2;
      g <= f by A1,A2;
      hence thesis by A3,WAYBEL_3:28;
    end;
  end;
  assume
A4: for i being Element of I holds f.i is_>=_than pi(X,i);
  let g be Element of product J;
  assume
A5: g in X;
  now
    let i be Element of I;
A6: f.i is_>=_than pi(X,i) by A4;
    g.i in pi(X,i) by A5,CARD_3:def 6;
    hence g.i <= f.i by A6;
  end;
  hence thesis by WAYBEL_3:28;
end;

theorem Th29:
  for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for f being Element of product J, X being Subset of product
J holds f is_<=_than X iff for i being Element of I holds f.i is_<=_than pi(X,i
  )
proof
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let f be Element of product J, X be Subset of product J;
  hereby
    assume
A1: f is_<=_than X;
    let i be Element of I;
    thus f.i is_<=_than pi(X, i)
    proof
      let x be Element of J.i;
      assume x in pi(X, i);
      then consider g being Function such that
A2:   g in X and
A3:   x = g.i by CARD_3:def 6;
      reconsider g as Element of product J by A2;
      g >= f by A1,A2;
      hence thesis by A3,WAYBEL_3:28;
    end;
  end;
  assume
A4: for i being Element of I holds f.i is_<=_than pi(X,i);
  let g be Element of product J;
  assume
A5: g in X;
  now
    let i be Element of I;
A6: f.i is_<=_than pi(X,i) by A4;
    g.i in pi(X,i) by A5,CARD_3:def 6;
    hence g.i >= f.i by A6;
  end;
  hence thesis by WAYBEL_3:28;
end;

theorem Th30:
  for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for X being Subset of product J holds ex_sup_of X, product J
  iff for i being Element of I holds ex_sup_of pi(X,i), J.i
proof
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let X be Subset of product J;
  hereby
    set f = sup X;
    assume
A1: ex_sup_of X, product J;
    let i be Element of I;
A2: now
      let x be Element of J.i;
      assume
A3:   pi(X,i) is_<=_than x;
      set g = f+*(i,x);
A4:   dom g = dom f by FUNCT_7:30;
      dom f = I by WAYBEL_3:27;
      then
A5:   g.i = x by FUNCT_7:31;
      now
        let j be Element of I;
        g.j = f.j or g.j = x & j = i by A5,FUNCT_7:32;
        hence g.j is Element of J.j;
      end;
      then reconsider g as Element of product J by A4,WAYBEL_3:27;
A6:   X is_<=_than f by A1,YELLOW_0:30;
      X is_<=_than g
      proof
        let h be Element of product J;
        assume
A7:     h in X;
        then
A8:     h.i in pi(X, i) by CARD_3:def 6;
A9:     h <= f by A6,A7;
        now
          let j be Element of I;
          g.j = f.j or g.j = x & j = i by A5,FUNCT_7:32;
          hence h.j <= g.j by A3,A9,A8,WAYBEL_3:28;
        end;
        hence h <= g by WAYBEL_3:28;
      end;
      then f <= g by A1,YELLOW_0:30;
      hence f.i <= x by A5,WAYBEL_3:28;
    end;
    f is_>=_than X by A1,YELLOW_0:30;
    then f.i is_>=_than pi(X, i) by Th28;
    hence ex_sup_of pi(X, i), J.i by A2,YELLOW_0:30;
  end;
  assume for i being Element of I holds ex_sup_of pi(X,i), J.i;
  then ex f being Element of product J st ( for i being Element of I holds f.i
  = sup pi(X,i))& f is_>=_than X & for g being Element of product J st X
  is_<=_than g holds f <= g by Lm1;
  hence thesis by YELLOW_0:30;
end;

theorem Th31:
  for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for X being Subset of product J holds ex_inf_of X, product J
  iff for i being Element of I holds ex_inf_of pi(X,i), J.i
proof
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let X be Subset of product J;
  hereby
    set f = inf X;
    assume
A1: ex_inf_of X, product J;
    let i be Element of I;
A2: f is_<=_than X by A1,YELLOW_0:31;
A3: now
      let x be Element of J.i;
      set g = f+*(i,x);
A4:   dom g = dom f by FUNCT_7:30;
      dom f = I by WAYBEL_3:27;
      then
A5:   g.i = x by FUNCT_7:31;
      now
        let j be Element of I;
        g.j = f.j or g.j = x & j = i by A5,FUNCT_7:32;
        hence g.j is Element of J.j;
      end;
      then reconsider g as Element of product J by A4,WAYBEL_3:27;
      assume
A6:   pi(X,i) is_>=_than x;
      X is_>=_than g
      proof
        let h be Element of product J;
        assume
A7:     h in X;
        then
A8:     h.i in pi(X, i) by CARD_3:def 6;
A9:     h >= f by A2,A7;
        now
          let j be Element of I;
          g.j = f.j or g.j = x & j = i by A5,FUNCT_7:32;
          hence h.j >= g.j by A6,A9,A8,WAYBEL_3:28;
        end;
        hence thesis by WAYBEL_3:28;
      end;
      then f >= g by A1,YELLOW_0:31;
      hence f.i >= x by A5,WAYBEL_3:28;
    end;
    f.i is_<=_than pi(X, i) by A2,Th29;
    hence ex_inf_of pi(X, i), J.i by A3,YELLOW_0:31;
  end;
  assume for i being Element of I holds ex_inf_of pi(X,i), J.i;
  then ex f being Element of product J st ( for i being Element of I holds f.i
  = inf pi(X,i))& f is_<=_than X & for g being Element of product J st X
  is_>=_than g holds f >= g by Lm2;
  hence thesis by YELLOW_0:31;
end;

theorem Th32:
  for I being non empty set for J being Poset-yielding non-Empty
  ManySortedSet of I for X being Subset of product J st ex_sup_of X, product J
  for i being Element of I holds (sup X).i = sup pi(X,i)
proof
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let X be Subset of product J;
  assume ex_sup_of X, product J;
  then for i being Element of I holds ex_sup_of pi(X,i), J.i by Th30;
  then consider f being Element of product J such that
A1: for i being Element of I holds f.i = sup pi(X,i) and
A2: f is_>=_than X and
A3: for g being Element of product J st X is_<=_than g holds f <= g by Lm1;
  sup X = f by A2,A3,YELLOW_0:30;
  hence thesis by A1;
end;

theorem Th33:
  for I being non empty set for J being Poset-yielding non-Empty
  ManySortedSet of I for X being Subset of product J st ex_inf_of X, product J
  for i being Element of I holds (inf X).i = inf pi(X,i)
proof
  let I be non empty set;
  let J be Poset-yielding non-Empty ManySortedSet of I;
  let X be Subset of product J;
  assume ex_inf_of X, product J;
  then for i being Element of I holds ex_inf_of pi(X,i), J.i by Th31;
  then consider f being Element of product J such that
A1: for i being Element of I holds f.i = inf pi(X,i) and
A2: f is_<=_than X and
A3: for g being Element of product J st X is_>=_than g holds f >= g by Lm2;
  inf X = f by A2,A3,YELLOW_0:31;
  hence thesis by A1;
end;

theorem Th34:
  for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I for X being directed Subset of product J
  for i being Element of I holds pi(X,i) is directed
proof
  let I be non empty set;
  let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
  let X be directed Subset of product J;
  let i be Element of I;
  let x,y be Element of J.i;
  assume x in pi(X,i);
  then consider f being Function such that
A1: f in X and
A2: x = f.i by CARD_3:def 6;
  assume y in pi(X,i);
  then consider g being Function such that
A3: g in X and
A4: y = g.i by CARD_3:def 6;
  reconsider f,g as Element of product J by A1,A3;
  consider h being Element of product J such that
A5: h in X and
A6: f <= h and
A7: g <= h by A1,A3,WAYBEL_0:def 1;
  take h.i;
  thus h.i in pi(X,i) by A5,CARD_3:def 6;
  thus thesis by A2,A4,A6,A7,WAYBEL_3:28;
end;

theorem Th35:
  for I being non empty set for J,K being RelStr-yielding
non-Empty ManySortedSet of I st for i being Element of I holds K.i is SubRelStr
  of J.i holds product K is SubRelStr of product J
proof
  let I be non empty set;
  let J,K be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds K.i is SubRelStr of J.i;
A2: now
    let i be object;
    assume i in I;
    then reconsider j = i as Element of I;
A3: ex R being 1-sorted st R = J.j & (Carrier J).j = the carrier of R by
PRALG_1:def 15;
A4: ex R being 1-sorted st R = K.j & (Carrier K).j = the carrier of R by
PRALG_1:def 15;
    K.j is SubRelStr of J.j by A1;
    hence (Carrier K).i c= (Carrier J).i by A3,A4,YELLOW_0:def 13;
  end;
A5: dom Carrier K = I by PARTFUN1:def 2;
A6: dom Carrier J = I by PARTFUN1:def 2;
A7: the carrier of product J = product Carrier J by YELLOW_1:def 4;
  the carrier of product K = product Carrier K by YELLOW_1:def 4;
  hence
A8: the carrier of product K c= the carrier of product J by A7,A6,A5,A2,
CARD_3:27;
  let x,y be object;
  assume
A9: [x,y] in the InternalRel of product K;
  reconsider x,y as Element of product K by A9,ZFMISC_1:87;
  reconsider f = x, g = y as Element of product J by A8;
A10: x <= y by A9,ORDERS_2:def 5;
  now
    let i be Element of I;
A11: x.i <= y.i by A10,WAYBEL_3:28;
    K.i is SubRelStr of J.i by A1;
    hence f.i <= g.i by A11,YELLOW_0:59;
  end;
  then f <= g by WAYBEL_3:28;
  hence thesis by ORDERS_2:def 5;
end;

theorem Th36:
  for I being non empty set for J,K being RelStr-yielding
  non-Empty ManySortedSet of I st for i being Element of I holds K.i is full
  SubRelStr of J.i holds product K is full SubRelStr of product J
proof
  let I be non empty set;
  let J,K be RelStr-yielding non-Empty ManySortedSet of I;
  assume
A1: for i being Element of I holds K.i is full SubRelStr of J.i;
  then for i being Element of I holds K.i is SubRelStr of J.i;
  then reconsider S = product K as non empty SubRelStr of product J by Th35;
A2: (the InternalRel of product J)|_2 the carrier of S = (the InternalRel of
  product J)/\[:the carrier of S,the carrier of S:] by WELLORD1:def 6;
  S is full
  proof
    the InternalRel of S c= the InternalRel of product J by YELLOW_0:def 13;
    hence
    the InternalRel of S c= (the InternalRel of product J)|_2 the carrier
    of S by A2,XBOOLE_1:19;
    let x,y be object;
    assume
A3: [x,y] in (the InternalRel of product J)|_2 the carrier of S;
    then
A4: [x,y] in the InternalRel of product J by A2,XBOOLE_0:def 4;
    [x,y] in [:the carrier of S, the carrier of S:] by A2,A3,XBOOLE_0:def 4;
    then reconsider x, y as Element of S by ZFMISC_1:87;
    reconsider a = x, b = y as Element of product J by YELLOW_0:58;
    reconsider x, y as Element of product K;
A5: a <= b by A4,ORDERS_2:def 5;
    now
      let i be Element of I;
A6:   K.i is full SubRelStr of J.i by A1;
      a.i <= b.i by A5,WAYBEL_3:28;
      hence x.i <= y.i by A6,YELLOW_0:60;
    end;
    then x <= y by WAYBEL_3:28;
    hence thesis by ORDERS_2:def 5;
  end;
  hence thesis;
end;

theorem
  for L being non empty RelStr, S being non empty SubRelStr of L, X
  being set holds S|^X is SubRelStr of L|^X
proof
  let L be non empty RelStr, S be non empty SubRelStr of L, X be set;
  per cases;
  suppose
A1: X = {};
    then
A2: L|^X = RelStr (#{{}}, id { {}}#) by YELLOW_1:27;
    S|^X = RelStr (#{{}}, id {{}}#) by A1,YELLOW_1:27;
    hence thesis by A2,YELLOW_6:6;
  end;
  suppose
    X <> {};
    then reconsider X as non empty set;
    for i be Element of X holds (X --> S).i is SubRelStr of (X --> L).i;
    hence thesis by Th35;
  end;
end;

theorem Th38:
  for L being non empty RelStr, S be full non empty SubRelStr of L
  , X be set holds S|^X is full SubRelStr of L|^X
proof
  let L be non empty RelStr, S be full non empty SubRelStr of L, X be set;
  per cases;
  suppose
A1: X = {};
    then
A2: L|^X = RelStr (#{{}},id {{}}#) by YELLOW_1:27;
    S|^X = RelStr (#{{}}, id {{}}#) by A1,YELLOW_1:27;
    hence thesis by A2,YELLOW_6:6;
  end;
  suppose
    X <> {};
    then reconsider X as non empty set;
    for i be Element of X holds (X --> S).i is full SubRelStr of (X --> L).i;
    hence thesis by Th36;
  end;
end;

begin :: Inheritance

definition
  let S,T be non empty RelStr, X be set;
  pred S inherits_sup_of X,T means

  ex_sup_of X,T implies "\/"(X, T) in the carrier of S;
  pred S inherits_inf_of X,T means

  ex_inf_of X,T implies "/\"(X, T) in the carrier of S;
end;

theorem
  for T being non empty transitive RelStr for S being full non
empty SubRelStr of T for X being Subset of S holds S inherits_sup_of X,T iff (
  ex_sup_of X,T implies ex_sup_of X, S & sup X = "\/"(X, T))
by YELLOW_0:64;

theorem
  for T being non empty transitive RelStr for S being full non empty
  SubRelStr of T for X being Subset of S holds S inherits_inf_of X,T iff (
  ex_inf_of X,T implies ex_inf_of X, S & inf X = "/\"(X, T))
by YELLOW_0:63;

scheme
  ProductSupsInheriting { I() -> non empty set, J,K() -> Poset-yielding
non-Empty ManySortedSet of I(), P[set, set] }: for X being Subset of product K(
  ) st P[X, product K()] holds product K() inherits_sup_of X, product J()
provided
A1: for X being Subset of product K() st P[X, product K()] for i being
Element of I() holds P[pi(X, i), K().i] and
A2: for i being Element of I() holds K().i is full SubRelStr of J().i and
A3: for i being Element of I(), X being Subset of K().i st P[X, K().i]
holds K().i inherits_sup_of X, J().i
proof
  let X be Subset of product K() such that
A4: P[X, product K()] and
A5: ex_sup_of X, product J();
  product K() is SubRelStr of product J() by A2,Th36;
  then the carrier of product K() c= the carrier of product J() by
YELLOW_0:def 13;
  then reconsider Y = X as Subset of product J() by XBOOLE_1:1;
  set f = "\/"(X, product J());
A6: now
    let i be Element of I();
A7: ex_sup_of pi(Y,i), J().i by A5,Th30;
    K().i inherits_sup_of pi(X, i), J().i by A1,A3,A4;
    then sup pi(Y,i) in the carrier of K().i by A7;
    hence f.i is Element of K().i by A5,Th32;
  end;
  dom f = I() by WAYBEL_3:27;
  then "\/"(X, product J()) is Element of product K() by A6,WAYBEL_3:27;
  hence thesis;
end;

scheme
  PowerSupsInheriting { I() -> non empty set, L() -> non empty Poset, S() ->
non empty full SubRelStr of L(), P[set, set] }: for X being Subset of S()|^I()
  st P[X, S()|^I()] holds S()|^I() inherits_sup_of X, L()|^I()
provided
A1: for X being Subset of S()|^I() st P[X, S()|^I()] for i being Element
of I() holds P[pi(X, i), S()] and
A2: for X being Subset of S() st P[X, S()] holds S() inherits_sup_of X, L()
proof
  reconsider K = I() --> S(), J = I() --> L() as Poset-yielding non-Empty
  ManySortedSet of I();
A3: for X be Subset of product K st P[X, product K] 
    for i be Element of I() holds P[pi(X, i), K.i] by A1;
A5: for i be Element of I(), X be Subset of K.i st P[X, K.i]
    holds K.i inherits_sup_of X, J.i by A2;
A8: for i be Element of I() holds K.i is full SubRelStr of J.i;
  for X being Subset of product K st P[X, product K] holds product K
  inherits_sup_of X, product J from ProductSupsInheriting(A3,A8,A5);
  hence thesis;
end;

scheme
  ProductInfsInheriting { I() -> non empty set, J,K() -> Poset-yielding
non-Empty ManySortedSet of I(), P[set, set] }: for X being Subset of product K(
  ) st P[X, product K()] holds product K() inherits_inf_of X, product J()
provided
A1: for X being Subset of product K() st P[X, product K()] for i being
Element of I() holds P[pi(X, i), K().i] and
A2: for i being Element of I() holds K().i is full SubRelStr of J().i and
A3: for i being Element of I(), X being Subset of K().i st P[X, K().i]
holds K().i inherits_inf_of X, J().i
proof
  let X be Subset of product K() such that
A4: P[X, product K()] and
A5: ex_inf_of X, product J();
  product K() is SubRelStr of product J() by A2,Th36;
  then the carrier of product K() c= the carrier of product J() by
YELLOW_0:def 13;
  then reconsider Y = X as Subset of product J() by XBOOLE_1:1;
  set f = "/\"(X, product J());
A6: now
    let i be Element of I();
A7: ex_inf_of pi(Y,i), J().i by A5,Th31;
    K().i inherits_inf_of pi(X, i), J().i by A1,A3,A4;
    then inf pi(Y,i) in the carrier of K().i by A7;
    hence f.i is Element of K().i by A5,Th33;
  end;
  dom f = I() by WAYBEL_3:27;
  then "/\"(X, product J()) is Element of product K() by A6,WAYBEL_3:27;
  hence thesis;
end;

scheme
  PowerInfsInheriting { I() -> non empty set, L() -> non empty Poset, S() ->
non empty full SubRelStr of L(), P[set, set] }: for X being Subset of S()|^I()
  st P[X, S()|^I()] holds S()|^I() inherits_inf_of X, L()|^I()
provided
A1: for X being Subset of S()|^I() st P[X, S()|^I()] for i being Element
of I() holds P[pi(X, i), S()] and
A2: for X being Subset of S() st P[X, S()] holds S() inherits_inf_of X, L()
proof
  reconsider K = I() --> S(), J = I() --> L() as Poset-yielding non-Empty
  ManySortedSet of I();
A3: for X be Subset of product K st P[X, product K]
    for i be Element of I() holds P[pi(X, i), K.i] by A1;
A5: for i be Element of I(), X be Subset of K.i st P[X, K.i] 
    holds K.i inherits_inf_of X, J.i by A2;
A8: for i be Element of I() holds K.i is full SubRelStr of J.i;
  for X being Subset of product K st P[X, product K] holds product K
  inherits_inf_of X, product J from ProductInfsInheriting(A3,A8,A5);
  hence thesis;
end;

registration
  let I be set;
  let L be non empty RelStr;
  let X be non empty Subset of L|^I;
  let i be set;
  cluster pi(X,i) -> non empty;
  coherence
  proof
    reconsider Y = X as non empty Subset of product (I --> L);
    set f = the Element of Y;
    reconsider f as Function;
    f.i in pi(X,i) by CARD_3:def 6;
    hence thesis;
  end;
end;

theorem
  for L being non empty Poset for S being directed-sups-inheriting non
  empty full SubRelStr of L for X be non empty set holds S|^X is
  directed-sups-inheriting SubRelStr of L|^X
proof
  let L be non empty Poset;
  let S be directed-sups-inheriting non empty full SubRelStr of L;
  let X be non empty set;
  reconsider SX = S|^X as full non empty SubRelStr of L|^X by Th38;
  defpred P[set, non empty reflexive RelStr] means $1 is directed non empty
  Subset of $2;
A1: now
    let A be Subset of S|^X;
    assume P[A,S|^X];
    then reconsider B = A as directed non empty Subset of S|^X;
    let i be Element of X;
    (X --> S).i = S;
    then pi(B, i) is directed non empty Subset of S by Th34;
    hence P[pi(A, i),S];
  end;
A2: now
    let X be Subset of S;
    assume P[X,S];
    then ex_sup_of X,L implies ex_sup_of X, S & sup X = "\/"(X, L) by
WAYBEL_0:7;
    hence S inherits_sup_of X, L;
  end;
  SX is directed-sups-inheriting
  proof
    let A be directed Subset of SX;
    for A being Subset of S|^X st P[A,S|^X] holds S|^X inherits_sup_of A,
    L|^X from PowerSupsInheriting(A1,A2);
    then A <> {} implies S|^X inherits_sup_of A, L|^X;
    hence thesis;
  end;
  hence thesis;
end;

registration
  let I be non empty set;
  let J be RelStr-yielding non-Empty ManySortedSet of I;
  let X be non empty Subset of product J;
  let i be set;
  cluster pi(X,i) -> non empty;
  coherence
  proof
    set f = the Element of X;
    reconsider f as Function;
    f.i in pi(X,i) by CARD_3:def 6;
    hence thesis;
  end;
end;

theorem Th42:
  for X being non empty set for L being up-complete non empty
  Poset holds L|^X is up-complete
proof
  let X be non empty set;
  let L be up-complete non empty Poset;
  now
    let A be non empty directed Subset of L|^X;
    reconsider B = A as non empty directed Subset of product (X --> L);
    now
      let x be Element of X;
      pi(B,x) is directed non empty by Th34;
      hence ex_sup_of pi(A,x), (X --> L).x by WAYBEL_0:75;
    end;
    hence ex_sup_of A,L|^X by Th30;
  end;
  hence thesis by WAYBEL_0:75;
end;

registration
  let L be up-complete non empty Poset;
  let X be non empty set;
  cluster L|^X -> up-complete;
  coherence by Th42;
end;

begin :: Topological retracts

theorem Th43:
  for T being non empty TopSpace, S being non empty SubSpace of T
  for f being Function of T,S st f is being_a_retraction holds rng f = the
  carrier of S
proof
  let T be non empty TopSpace, S be non empty SubSpace of T;
  let f be Function of T,S such that
A1: for W being Point of T st W in the carrier of S holds f.W=W;
  thus rng f c= the carrier of S;
  let x be object;
A2: [#]S = the carrier of S;
  [#]T = the carrier of T;
  then
A3: the carrier of S c= the carrier of T by A2,PRE_TOPC:def 4;
  assume
A4: x in the carrier of S;
  then x in the carrier of T by A3;
  then
A5: x in dom f by FUNCT_2:def 1;
  f.x = x by A1,A3,A4;
  hence thesis by A5,FUNCT_1:def 3;
end;

theorem
  for T being non empty TopSpace, S being non empty SubSpace of T for f
  being continuous Function of T,S st f is being_a_retraction holds f is
  idempotent
proof
  let T be non empty TopSpace, S be non empty SubSpace of T;
A1: [#]S = the carrier of S;
  let f be continuous Function of T,S such that
A2: f is being_a_retraction;
A3: rng f = the carrier of S by A2,Th43;
A4: dom f = the carrier of T by FUNCT_2:def 1;
  [#]T = the carrier of T;
  then
A5: the carrier of S c= the carrier of T by A1,PRE_TOPC:def 4;
A6: now
    let x be object;
    assume
A7: x in the carrier of T;
    then
A8: f.x in rng f by A4,FUNCT_1:def 3;
    (f*f).x = f.(f.x) by A4,A7,FUNCT_1:13;
    hence (f*f).x = f.x by A2,A5,A3,A8;
  end;
  dom (f*f) = the carrier of T by A5,A4,A3,RELAT_1:27;
  then f*f = f by A4,A6,FUNCT_1:2;
  hence thesis by QUANTAL1:def 9;
end;

theorem Th45:
  for T being non empty TopSpace, V being open Subset of T holds
  chi(V, the carrier of T) is continuous Function of T, Sierpinski_Space
proof
  let T be non empty TopSpace, V be open Subset of T;
  reconsider c = chi(V, the carrier of T) as Function of T, Sierpinski_Space
  by WAYBEL18:def 9;
A1: c"{0,1} = [#]T by FUNCT_2:40;
  c = chi(c"{1}, the carrier of T) by FUNCT_3:40;
  then
A2: V = c"{1} by FUNCT_3:38;
A3: c"{} = {}T;
A4: now
    let W be Subset of Sierpinski_Space;
    assume W is open;
    then W in the topology of Sierpinski_Space by PRE_TOPC:def 2;
    then W in {{}, {1}, {0,1}} by WAYBEL18:def 9;
    hence c"W is open by A2,A3,A1,ENUMSET1:def 1;
  end;
  [#]Sierpinski_Space <> {};
  hence thesis by A4,TOPS_2:43;
end;

theorem
  for T being non empty TopSpace, x,y being Element of T st for W being
  open Subset of T st y in W holds x in W holds (0,1) --> (y,x) is continuous
  Function of Sierpinski_Space, T
proof
  let T be non empty TopSpace;
  let x,y be Element of T such that
A1: for W being open Subset of T st y in W holds x in W;
A2: the carrier of Sierpinski_Space = {0,{0}} by WAYBEL18:def 9, CARD_1:49;
  then reconsider i = (0,{0}) --> (y,x) as Function of Sierpinski_Space, T;
A3: i.1 = x by FUNCT_4:63, CARD_1:49;
A4: not 1 in {0} by TARSKI:def 1;
A5: 0 in {0} by TARSKI:def 1;
A6: 1 in {0,1} by TARSKI:def 2;
A7: i.0 = y by FUNCT_4:63;
A8: now
    let W be Subset of T;
    assume W is open;
    then
A9: y in W & x in W or not y in W & x in W or not y in W & not x in W by A1;
A10:  i"W = {} or i"W = {0} or i"W = {1} or i"W = {0,1}
          by A2,ZFMISC_1:36, CARD_1:49;
    i"W <> {0} by A7,A3,A6,A5,A4,A9,FUNCT_2:38, CARD_1:49;
    then i"W in {{}, {1}, {0,1}}
     by ENUMSET1:def 1,A10;
    then i"W in the topology of Sierpinski_Space by WAYBEL18:def 9;
    hence i"W is open by PRE_TOPC:def 2;
  end;
  [#]T <> {};
  hence thesis by A8,TOPS_2:43, CARD_1:49;
end;

theorem
  for T being non empty TopSpace, x,y being Element of T for V being
  open Subset of T st x in V & not y in V holds chi(V, the carrier of T)*
   ((0,1) --> (y,x)) = id Sierpinski_Space
proof
  let T be non empty TopSpace;
  let x,y be Element of T, V be open Subset of T such that
A1: x in V and
A2: not y in V;
  reconsider c = chi(V, the carrier of T) as Function of T, Sierpinski_Space
  by Th45;
A3: c.x = 1 by A1,FUNCT_3:def 3;
A4: the carrier of Sierpinski_Space = {0,{0}} by WAYBEL18:def 9, CARD_1:49;
  then reconsider i = (0,{0}) --> (y,x) as Function of Sierpinski_Space, T;
A5: i.1 = x by FUNCT_4:63, CARD_1:49;
A6: c.y = 0 by A2,FUNCT_3:def 3;
A7: i.0 = y by FUNCT_4:63;
  now
    thus c*i is Function of Sierpinski_Space, Sierpinski_Space;
    let a be Element of Sierpinski_Space;
    a = 0 or a = 1 by A4,TARSKI:def 2, CARD_1:49;
    hence (c*i).a = a by A7,A5,A3,A6,FUNCT_2:15
      .= (id Sierpinski_Space).a;
  end;
  hence thesis by FUNCT_2:63, CARD_1:49;
end;

theorem
  for T being non empty 1-sorted, V,W being Subset of T for S being
  TopAugmentation of BoolePoset{0}
    for f, g being Function of T, S st f = chi(V,
  the carrier of T) & g = chi(W, the carrier of T) holds V c= W iff f <= g
proof
  let T be non empty 1-sorted, V,W be Subset of T;
  let S be TopAugmentation of BoolePoset{0};
  let c1, c2 be Function of T, S such that
A1: c1 = chi(V, the carrier of T) and
A2: c2 = chi(W, the carrier of T);
A3: the RelStr of S = BoolePoset{0} by YELLOW_9:def 4;
  hereby
    assume
A4: V c= W;
    now
      let z be set;
      assume z in the carrier of T;
      then reconsider x = z as Element of T;
      reconsider a = c1.x, b = c2.x as Element of BoolePoset{0} by A3;
      x in V & x in W or not x in V by A4;
      then c1.x = 1 & c2.x = 1 or c1.x = 0 by A1,A2,FUNCT_3:def 3;
      then c1.x c= c2.x;
      then a <= b by YELLOW_1:2;
      hence ex a,b being Element of S st a = c1.z & b = c2.z & a <= b by A3,
YELLOW_0:1;
    end;
    hence c1 <= c2;
  end;
  assume
A5: c1 <= c2;
  let x be object;
  assume that
A6: x in V and
A7: not x in W;
  reconsider x as Element of T by A6;
A8: c2.x = 0 by A2,A7,FUNCT_3:def 3;
A9: 0 c= {0};
  reconsider a = c1.x, b = c2.x as Element of BoolePoset{0} by A3;
  ex a,b being Element of S st a = c1.x & b = c2.x & a <= b by A5;
  then
A10: a <= b by A3,YELLOW_0:1;
  c1.x = 1 by A1,A6,FUNCT_3:def 3;
  then {0} c= 0 by A8,A10,YELLOW_1:2,CARD_1:49;
  hence thesis by A9,XBOOLE_0:def 10;
end;

theorem
  for L being non empty RelStr, X being non empty set for R being full
non empty SubRelStr of L|^X st for a being set holds a is Element of R iff ex x
  being Element of L st a = X --> x holds L, R are_isomorphic
proof
  let L be non empty RelStr, X be non empty set;
  deffunc F(set) = X --> $1;
  consider f being ManySortedSet of the carrier of L such that
A1: for i being Element of L holds f.i = F(i) from PBOOLE:sch 5;
  let R be full non empty SubRelStr of L|^X such that
A2: for a being set holds a is Element of R iff ex x being Element of L
  st a = X --> x;
A3: rng f c= the carrier of R
  proof
    let y be object;
    assume y in rng f;
    then consider x being object such that
A4: x in dom f and
A5: y = f.x by FUNCT_1:def 3;
    reconsider x as Element of L by A4;
    y = X --> x by A1,A5;
    then y is Element of R by A2;
    hence thesis;
  end;
A6: dom f = the carrier of L by PARTFUN1:def 2;
  then reconsider f as Function of L, R by A3,FUNCT_2:2;
A7: f is one-to-one
  proof
    let x,y be Element of L;
    f.y = X --> y by A1;
    then
A8: f.y = [:X,{y}:] by FUNCOP_1:def 2;
    f.x = X --> x by A1;
    then f.x = [:X,{x}:] by FUNCOP_1:def 2;
    then f.x = f.y implies {x} = {y} by A8,ZFMISC_1:110;
    hence thesis by ZFMISC_1:3;
  end;
A9: now
    set i = the Element of X;
    let x,y be Element of L;
    reconsider a = f.x, b = f.y as Element of L|^X by YELLOW_0:58;
    reconsider Xx = X --> x, Xy = X --> y as Function of X,L;
    reconsider a9 = a, b9 = b as Element of product (X --> L);
A11: f.y = X --> y by A1;
A12: f.x = X --> x by A1;
    hereby
      assume
A13:  x <= y;
      Xx <= Xy
      proof
        let i be set;
        assume
A14:    i in X;
        then
A15:    (X --> y).i = y by FUNCOP_1:7;
        (X --> x).i = x by A14,FUNCOP_1:7;
        hence thesis by A13,A15;
      end;
      then a <= b by A12,A11,WAYBEL10:11;
      hence f.x <= f.y by YELLOW_0:60;
    end;
    assume f.x <= f.y;
    then a <= b by YELLOW_0:59;
    then a9.i <= b9.i by WAYBEL_3:28;
    then x <= Xy.i by A12,A11;
    hence x <= y;
  end;
  take f;
  rng f = the carrier of R
  proof
    thus rng f c= the carrier of R;
    let x be object;
    assume x in the carrier of R;
    then reconsider a = x as Element of R;
    consider i being Element of L such that
A16: a = X --> i by A2;
    a = f.i by A1,A16;
    hence thesis by A6,FUNCT_1:def 3;
  end;
  hence thesis by A7,A9,WAYBEL_0:66;
end;

theorem
  for S,T being non empty TopSpace holds S, T are_homeomorphic iff ex f
  being continuous Function of S,T, g being continuous Function of T,S st f*g =
  id T & g*f = id S
proof
  let S,T be non empty TopSpace;
  hereby
    assume S, T are_homeomorphic;
    then consider f being Function of S,T such that
A1: f is being_homeomorphism;
    reconsider f as continuous Function of S,T by A1,TOPS_2:def 5;
A2: rng f = [#]T by A1,TOPS_2:def 5;
    reconsider g = f" as continuous Function of T,S by A1,TOPS_2:def 5;
    take f,g;
A3: dom f = [#]S by A1,TOPS_2:def 5;
    f is one-to-one by A1,TOPS_2:def 5;
    hence f*g = id T & g*f = id S by A2,A3,TOPS_2:52;
  end;
  given f being continuous Function of S,T, g being continuous Function of T,S
  such that
A4: f*g = id T and
A5: g*f = id S;
A6: f is onto by A4,FUNCT_2:23;
    then
A7: rng f = [#]T by FUNCT_2:def 3;
  take f;
A8: dom f = [#]S by FUNCT_2:def 1;
A9: f is one-to-one by A5,FUNCT_2:23;
  then g = f qua Function" by A5,A7,FUNCT_2:30
    .= f" by A6,A9,TOPS_2:def 4;
  hence thesis by A9,A7,A8,TOPS_2:def 5;
end;

theorem Th51:
  for T, S, R being non empty TopSpace for f being Function of T,S
  , g being Function of S,T, h being Function of S, R st f*g = id S & h is
  being_homeomorphism holds (h*f)*(g*(h")) = id R
proof
  let T, S, R be non empty TopSpace;
  let f be Function of T,S, g be Function of S,T, h be Function of S, R such
  that
A1: f*g = id S and
A2: h is being_homeomorphism;
A3: h is one-to-one by A2,TOPS_2:def 5;
A4: rng h = [#]R by A2,TOPS_2:def 5;
  thus (h*f)*(g*(h")) = (h*f)*g*(h") by RELAT_1:36
    .= h*(id the carrier of S)*(h") by A1,RELAT_1:36
    .= h*(h") by FUNCT_2:17
    .= id R by A3,A4,TOPS_2:52;
end;

theorem Th52:
  for T, S, R being non empty TopSpace st S is_Retract_of T & S, R
  are_homeomorphic holds R is_Retract_of T
proof
  let T, S, R be non empty TopSpace;
  given f being continuous Function of S,T, g being continuous Function of T,S
  such that
A1: g*f = id S;
  given h being Function of S,R such that
A2: h is being_homeomorphism;
  h" is continuous by A2,TOPS_2:def 5;
  then reconsider f9 = f*(h") as continuous Function of R,T;
  h is continuous by A2,TOPS_2:def 5;
  then reconsider g9 = h*g as continuous Function of T,R;
  take f9,g9;
  thus thesis by A1,A2,Th51;
end;

theorem Th53:
  for T being non empty TopSpace, S being non empty SubSpace of T
  holds incl(S,T) is continuous
proof
  let T be non empty TopSpace, S be non empty SubSpace of T;
  incl(S,T) = id S by BORSUK_1:1,YELLOW_9:def 1;
  hence thesis by PRE_TOPC:26;
end;

theorem Th54:
  for T being non empty TopSpace for S being non empty SubSpace of
T, f being continuous Function of T,S st f is being_a_retraction holds f*incl(S
  ,T) = id S
proof
  let T be non empty TopSpace, S be non empty SubSpace of T;
  let f be continuous Function of T,S such that
A1: f is being_a_retraction;
A2: [#]S = the carrier of S;
  [#]T = the carrier of T;
  then
A3: the carrier of S c= the carrier of T by A2,PRE_TOPC:def 4;
  then
A4: incl(S,T) = id the carrier of S by YELLOW_9:def 1;
  now
    let x be Element of S;
    reconsider y = x as Point of T by A3;
    thus (f*incl(S,T)).x = f.((incl(S,T)).x) by FUNCT_2:15
      .= f.x by A4
      .= y by A1
      .= (id S).x;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th55:
  for T being non empty TopSpace, S being non empty SubSpace of T
  st S is_a_retract_of T holds S is_Retract_of T
proof
  let T be non empty TopSpace, S be non empty SubSpace of T;
  reconsider g = incl(S,T) as continuous Function of S,T by Th53;
  given f be continuous Function of T,S such that
A1: f is being_a_retraction;
  take g,f;
  thus thesis by A1,Th54;
end;

theorem
  for R,T being non empty TopSpace holds R is_Retract_of T iff ex S
  being non empty SubSpace of T st S is_a_retract_of T & S,R are_homeomorphic
proof
  let R,T be non empty TopSpace;
  hereby
    assume R is_Retract_of T;
    then consider f being Function of T,T such that
A1: f is continuous and
A2: f*f = f and
A3: Image f, R are_homeomorphic by WAYBEL18:def 8;
    reconsider S = Image f as non empty SubSpace of T;
    f = corestr f by WAYBEL18:def 7;
    then reconsider f as continuous Function of T,S by A1,WAYBEL18:10;
    take S;
A4: [#]T = the carrier of T;
    [#]S = the carrier of S;
    then the carrier of S c= the carrier of T by A4,PRE_TOPC:def 4;
    then reconsider rf = rng f as Subset of T by XBOOLE_1:1;
    now
      let x be Point of T;
      assume x in the carrier of S;
      then x in [#](T|rf) by WAYBEL18:def 6;
      then x in rng f by PRE_TOPC:def 5;
      then ex y being object st y in dom f & x = f.y by FUNCT_1:def 3;
      hence f.x = x by A2,FUNCT_1:13;
    end;
    then f is being_a_retraction;
    hence S is_a_retract_of T & S, R are_homeomorphic by A3;
  end;
  given S being non empty SubSpace of T such that
A5: S is_a_retract_of T and
A6: S,R are_homeomorphic;
  thus thesis by A5,A6,Th52,Th55;
end;