:: YELLOW16 semantic presentation

begin

theorem :: YELLOW16:1
canceled;

theorem :: YELLOW16:2
for X being set
for L being non empty RelStr
for 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 ; ::_thesis: for L being non empty RelStr
for 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
let L be non empty RelStr ; ::_thesis: for 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
let S be non empty SubRelStr of L; ::_thesis: 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
let f, g be Function of X, the carrier of S; ::_thesis: for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f <= g holds
f9 <= g9
let f9, g9 be Function of X, the carrier of L; ::_thesis: ( f9 = f & g9 = g & f <= g implies f9 <= g9 )
assume that
A1: f9 = f and
A2: g9 = g and
A3: f <= g ; ::_thesis: f9 <= g9
let x be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not x in X or ex b1, b2 being Element of the carrier of L st
( b1 = f9 . x & b2 = g9 . x & b1 <= b2 ) )
assume A4: x in X ; ::_thesis: ex b1, b2 being Element of the carrier of L st
( b1 = f9 . x & b2 = g9 . x & b1 <= b2 )
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 ; ::_thesis: ex b1 being Element of the carrier of L st
( a9 = f9 . x & b1 = g9 . x & a9 <= b1 )
take  b9 ; ::_thesis: ( a9 = f9 . x & b9 = g9 . x & a9 <= b9 )
thus  ( a9 = f9 . x & b9 = g9 . x ) by A1, A2; ::_thesis: a9 <= b9
 ex a, b being Element of S st
( a = f . x & b = g . x & a <= b ) by A3, A4, YELLOW_2:def_1;
hence  a9 <= b9 by YELLOW_0:59; ::_thesis: verum
end;

theorem :: YELLOW16:3
for X being set
for L being non empty RelStr
for S being non empty full 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 ; ::_thesis: for L being non empty RelStr
for S being non empty full 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
let L be non empty RelStr ; ::_thesis: for S being non empty full 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
let S be non empty full SubRelStr of L; ::_thesis: 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
let f, g be Function of X, the carrier of S; ::_thesis: for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds
f <= g
let f9, g9 be Function of X, the carrier of L; ::_thesis: ( f9 = f & g9 = g & f9 <= g9 implies f <= g )
assume that
A1: f9 = f and
A2: g9 = g and
A3: f9 <= g9 ; ::_thesis: f <= g
let x be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not x in X or ex b1, b2 being Element of the carrier of S st
( b1 = f . x & b2 = g . x & b1 <= b2 ) )
assume A4: x in X ; ::_thesis: ex b1, b2 being Element of the carrier of S st
( b1 = f . x & b2 = g . x & b1 <= b2 )
then reconsider a = f . x, b = g . x as Element of S by FUNCT_2:5;
take  a ; ::_thesis: ex b1 being Element of the carrier of S st
( a = f . x & b1 = g . x & a <= b1 )
take  b ; ::_thesis: ( a = f . x & b = g . x & a <= b )
thus  ( a = f . x & b = g . x ) ; ::_thesis: a <= b
 ex a9, b9 being Element of L st
( a9 = a & b9 = b & a9 <= b9 ) by A1, A2, A3, A4, YELLOW_2:def_1;
hence  a <= b by YELLOW_0:60; ::_thesis: verum
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V24( the carrier of S) quasi_total monotone directed-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st
( b1 is directed-sups-preserving & b1 is monotone )
proof
set x = the Element of T;
take f = S --> the Element of T; ::_thesis: ( f is directed-sups-preserving & f is monotone )
thus  f is directed-sups-preserving ::_thesis: f is monotone
proof
let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or f preserves_sup_of X )
assume A1: ( not X is empty & X is directed ) ; ::_thesis: f preserves_sup_of X
A2: f .: X = { the Element of T}
proof
set a = the Element of X;
thus  f .: X c= { the Element of T} by FUNCOP_1:81; :: according to XBOOLE_0:def_10 ::_thesis: { the Element of T} c= f .: X
A3: dom f = the carrier of S by FUNCOP_1:13;
A4: the Element of X in X by A1;
then  f . the Element of X = the Element of T by FUNCOP_1:7;
then  the Element of T in f .: X by A4, A3, FUNCT_1:def_6;
hence  { the Element of T} c= f .: X by ZFMISC_1:31; ::_thesis: verum
end;
assume  ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,S)) )
thus  ex_sup_of f .: X,T by A2, YELLOW_0:38; ::_thesis: "\/" ((f .: X),T) = f . ("\/" (X,S))
thus  sup (f .: X) = the Element of T by A2, YELLOW_0:39
.= f . (sup X) by FUNCOP_1:7 ; ::_thesis: verum
end;
let a, b be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not a <= b or f . a <= f . b )
A5: the Element of T <= the Element of T ;
 f . a = the Element of T by FUNCOP_1:7;
hence  ( not a <= b or f . a <= f . b ) by A5, FUNCOP_1:7; ::_thesis: verum
end;
end;

theorem :: YELLOW16:4
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; ::_thesis: ( f is idempotent & rng g c= rng f & rng g c= dom f implies f * g = g )
assume  f is idempotent ; ::_thesis: ( not rng g c= rng f or not rng g c= dom f or f * g = g )
then A1: f * f = f by QUANTAL1:def_9;
assume A2: rng g c= rng f ; ::_thesis: ( not rng g c= dom f or f * g = g )
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
(f_*_g)_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom g implies (f * g) . x = g . x )
assume A4: x in dom g ; ::_thesis: (f * g) . x = g . x
then  g . x in rng g by FUNCT_1:def_3;
then A5: ex a being set 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; ::_thesis: verum
end;
assume  rng g c= dom f ; ::_thesis: f * g = g
then  dom (f * g) = dom g by RELAT_1:27;
hence  f * g = g by A3, FUNCT_1:2; ::_thesis: verum
end;

registration
let S be 1-sorted ;
cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like V24( the carrier of S) quasi_total idempotent for Element of bool [: the carrier of S, the carrier of S:];
existence
 ex b1 being Function of S,S st b1 is idempotent
proof
take f = id S; ::_thesis: f is idempotent
 f * f = f by FUNCT_2:17;
hence  f is idempotent by QUANTAL1:def_9; ::_thesis: verum
end;
end;

theorem Th5: :: YELLOW16:5
for L being non empty up-complete Poset
for S being non empty full directed-sups-inheriting SubRelStr of L holds S is up-complete
proof
let L be non empty up-complete Poset; ::_thesis: for S being non empty full directed-sups-inheriting SubRelStr of L holds S is up-complete
let S be non empty full directed-sups-inheriting SubRelStr of L; ::_thesis: S is up-complete
now__::_thesis:_for_X_being_non_empty_directed_Subset_of_S_holds_ex_sup_of_X,S
let X be non empty directed Subset of S; ::_thesis: ex_sup_of X,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; ::_thesis: verum
end;
hence  S is up-complete by WAYBEL_0:75; ::_thesis: verum
end;

theorem Th6: :: YELLOW16:6
for L being non empty up-complete Poset
for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
Image f is directed-sups-inheriting
proof
let L be non empty up-complete Poset; ::_thesis: for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
Image f is directed-sups-inheriting
let f be Function of L,L; ::_thesis: ( f is idempotent & f is directed-sups-preserving implies Image f is directed-sups-inheriting )
set S = subrelstr (rng f);
set a = the Element of L;
reconsider S9 = subrelstr (rng f) as non empty full SubRelStr of L ;
assume A1: ( f is idempotent & f is directed-sups-preserving ) ; ::_thesis: Image f is directed-sups-inheriting
 subrelstr (rng f) is directed-sups-inheriting
proof
let X be directed Subset of (subrelstr (rng f)); :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr (rng f)) )
 X c= the carrier of (subrelstr (rng f)) ;
then A2: X c= rng f by YELLOW_0:def_15;
assume  X <> {} ; ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr (rng f)) )
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 ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr (rng f))
 f preserves_sup_of X9 by A1, WAYBEL_0:def_37;
then  sup (f .: X9) = f . (sup X9) by A3, WAYBEL_0:def_31;
then  sup X9 = f . (sup X9) by A1, A2, YELLOW_2:20;
then  "\/" (X,L) in rng f by FUNCT_2:4;
hence  "\/" (X,L) in the carrier of (subrelstr (rng f)) by YELLOW_0:def_15; ::_thesis: verum
end;
hence  Image f is directed-sups-inheriting ; ::_thesis: verum
end;

theorem Th7: :: YELLOW16:7
for T being non empty RelStr
for S being non empty SubRelStr of T
for f being Function of T,S st f * (incl (S,T)) = id S holds
f is idempotent Function of T,T
proof
let T be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of T
for f being Function of T,S st f * (incl (S,T)) = id S holds
f is idempotent Function of T,T
let S be non empty SubRelStr of T; ::_thesis: for f being Function of T,S st f * (incl (S,T)) = id S holds
f is idempotent Function of T,T
let f be Function of T,S; ::_thesis: ( f * (incl (S,T)) = id S implies f is idempotent Function of T,T )
assume A1: f * (incl (S,T)) = id S ; ::_thesis: f is idempotent Function of T,T
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  f is idempotent Function of T,T by A2, A3, A4, FUNCT_2:2, QUANTAL1:def_9; ::_thesis: verum
end;

definition
let S, T be non empty Poset;
let f be Function;
predf is_a_retraction_of T,S means :Def1: :: YELLOW16:def 1
( f is directed-sups-preserving Function of T,S & f | the carrier of S = id S & S is full directed-sups-inheriting SubRelStr of T );
predf is_an_UPS_retraction_of T,S means :Def2: :: YELLOW16:def 2
( 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;

:: deftheorem Def1 defines is_a_retraction_of YELLOW16:def_1_:_
 for S, T being non empty Poset
for f being Function holds
( f is_a_retraction_of T,S iff ( f is directed-sups-preserving Function of T,S & f | the carrier of S = id S & S is full directed-sups-inheriting SubRelStr of T ) );

:: deftheorem Def2 defines is_an_UPS_retraction_of YELLOW16:def_2_:_
 for S, T being non empty Poset
for f being Function holds
( f is_an_UPS_retraction_of T,S iff ( f is directed-sups-preserving Function of T,S & ex g being directed-sups-preserving Function of S,T st f * g = id S ) );

definition
let S, T be non empty Poset;
predS is_a_retract_of T means :Def3: :: YELLOW16:def 3
 ex f being Function of T,S st f is_a_retraction_of T,S;
predS is_an_UPS_retract_of T means :Def4: :: YELLOW16:def 4
 ex f being Function of T,S st f is_an_UPS_retraction_of T,S;
end;

:: deftheorem Def3 defines is_a_retract_of YELLOW16:def_3_:_
 for S, T being non empty Poset holds
( S is_a_retract_of T iff ex f being Function of T,S st f is_a_retraction_of T,S );

:: deftheorem Def4 defines is_an_UPS_retract_of YELLOW16:def_4_:_
 for S, T being non empty Poset holds
( S is_an_UPS_retract_of T iff ex f being Function of T,S st f is_an_UPS_retraction_of T,S );

theorem Th8: :: YELLOW16:8
for S, T being non empty Poset
for 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; ::_thesis: for f being Function st f is_a_retraction_of T,S holds
f * (incl (S,T)) = id S
let f be Function; ::_thesis: ( f is_a_retraction_of T,S implies f * (incl (S,T)) = id S )
assume that
 f is directed-sups-preserving Function of T,S and
A1: f | the carrier of S = id S and
A2: S is full directed-sups-inheriting SubRelStr of T ; :: according to YELLOW16:def_1 ::_thesis: f * (incl (S,T)) = id S
 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 ;
::_thesis: verum
end;

theorem Th9: :: YELLOW16:9
for S being non empty Poset
for T being non empty up-complete 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; ::_thesis: for T being non empty up-complete Poset
for f being Function st f is_a_retraction_of T,S holds
f is_an_UPS_retraction_of T,S
let T be non empty up-complete Poset; ::_thesis: for f being Function st f is_a_retraction_of T,S holds
f is_an_UPS_retraction_of T,S
let f be Function; ::_thesis: ( f is_a_retraction_of T,S implies f is_an_UPS_retraction_of T,S )
assume A1: f is_a_retraction_of T,S ; ::_thesis: f is_an_UPS_retraction_of T,S
hence  f is directed-sups-preserving Function of T,S by Def1; :: according to YELLOW16:def_2 ::_thesis: ex g being directed-sups-preserving Function of S,T st f * g = id S
 S is full directed-sups-inheriting SubRelStr of T by A1, Def1;
then reconsider g = incl (S,T) as directed-sups-preserving Function of S,T by WAYBEL21:10;
take  g ; ::_thesis: f * g = id S
thus  f * g = id S by A1, Th8; ::_thesis: verum
end;

theorem Th10: :: YELLOW16:10
for S, T being non empty Poset
for 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; ::_thesis: for f being Function st f is_a_retraction_of T,S holds
rng f = the carrier of S
let f be Function; ::_thesis: ( f is_a_retraction_of T,S implies rng f = the carrier of S )
assume A1: f is_a_retraction_of T,S ; ::_thesis: rng f = the carrier of S
then reconsider f = f as Function of T,S by Def1;
 f * (incl (S,T)) = id S by A1, Th8;
then  f is onto by FUNCT_2:23;
hence  rng f = the carrier of S by FUNCT_2:def_3; ::_thesis: verum
end;

theorem Th11: :: YELLOW16:11
for S, T being non empty Poset
for 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; ::_thesis: for f being Function st f is_an_UPS_retraction_of T,S holds
rng f = the carrier of S
let f be Function; ::_thesis: ( f is_an_UPS_retraction_of T,S implies rng f = the carrier of S )
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 ; :: according to YELLOW16:def_2 ::_thesis: rng f = the carrier of S
reconsider f = f as Function of T,S by A1;
 f is onto by A2, FUNCT_2:23;
hence  rng f = the carrier of S by FUNCT_2:def_3; ::_thesis: verum
end;

theorem Th12: :: YELLOW16:12
for S, T being non empty Poset
for 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; ::_thesis: for f being Function st f is_a_retraction_of T,S holds
f is idempotent Function of T,T
let f be Function; ::_thesis: ( f is_a_retraction_of T,S implies f is idempotent Function of T,T )
assume A1: f is_a_retraction_of T,S ; ::_thesis: f is idempotent Function of T,T
then A2: f is Function of T,S by Def1;
A3: S is SubRelStr of T by A1, Def1;
 f * (incl (S,T)) = id S by A1, Th8;
hence  f is idempotent Function of T,T by A2, A3, Th7; ::_thesis: verum
end;

theorem Th13: :: YELLOW16:13
for T, S being non empty Poset
for f being Function of T,T st f is_a_retraction_of T,S holds
Image f = RelStr(# the carrier of S, the InternalRel of S #)
proof
let T, S be non empty Poset; ::_thesis: for f being Function of T,T st f is_a_retraction_of T,S holds
Image f = RelStr(# the carrier of S, the InternalRel of S #)
let f be Function of T,T; ::_thesis: ( f is_a_retraction_of T,S implies Image f = RelStr(# the carrier of S, the InternalRel of S #) )
A1: the carrier of (Image f) = rng f by YELLOW_0:def_15;
assume A2: f is_a_retraction_of T,S ; ::_thesis: Image f = RelStr(# the carrier of S, the InternalRel of S #)
then  S is full SubRelStr of T by Def1;
hence  Image f = RelStr(# the carrier of S, the InternalRel of S #) by A2, A1, Th10, YELLOW_0:57; ::_thesis: verum
end;

theorem Th14: :: YELLOW16:14
for T being non empty up-complete Poset
for S being non empty Poset
for f being Function of T,T st f is_a_retraction_of T,S holds
( f is directed-sups-preserving & f is projection )
proof
let T be non empty up-complete Poset; ::_thesis: for S being non empty Poset
for f being Function of T,T st f is_a_retraction_of T,S holds
( f is directed-sups-preserving & f is projection )
let S be non empty Poset; ::_thesis: for f being Function of T,T st f is_a_retraction_of T,S holds
( f is directed-sups-preserving & f is projection )
let f be Function of T,T; ::_thesis: ( f is_a_retraction_of T,S implies ( f is directed-sups-preserving & f is projection ) )
assume A1: f is_a_retraction_of T,S ; ::_thesis: ( f is directed-sups-preserving & f is projection )
then reconsider g = f as directed-sups-preserving Function of T,S by Def1;
 f is idempotent by A1, Th12;
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, Th9, Th11
.= (id S) * f by A1, Def1
.= (id the carrier of S) * g ;
A3: S is non empty full directed-sups-inheriting SubRelStr of T by A1, Def1;
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; ::_thesis: f is projection
 f is idempotent directed-sups-preserving Function of T,T by A1, A2, A4, A5, Th12, WAYBEL20:28;
hence  f is projection by WAYBEL_1:def_13; ::_thesis: verum
end;

theorem Th15: :: YELLOW16:15
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 ; ::_thesis: 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 ) ) )
let f be Function of S,T; ::_thesis: ( f is isomorphic iff ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) ) )
hereby  ::_thesis: ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) implies f is isomorphic )
assume A1: f is isomorphic ; ::_thesis: ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) )
hence  f is monotone ; ::_thesis: ex g being monotone Function of T,S st
( f * g = id T & g * f = id S )
consider g being Function of T,S such that
A2: g = f " and
A3: g is monotone by A1, WAYBEL_0:def_38;
reconsider g = g as monotone Function of T,S by A3;
take g = g; ::_thesis: ( f * g = id T & g * f = id S )
 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; ::_thesis: verum
end;
assume A4: f is monotone ; ::_thesis: ( for g being monotone Function of T,S holds
( not f * g = id T or not g * f = id S ) or f is isomorphic )
given g being monotone Function of T,S such that A5: f * g = id T and
A6: g * f = id S ; ::_thesis: f is isomorphic
A7: f is V7() 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 " by A6, A7, FUNCT_2:30;
hence  f is isomorphic by A4, A7, WAYBEL_0:def_38; ::_thesis: verum
end;

theorem Th16: :: YELLOW16:16
for S, T being non empty Poset holds
( S,T are_isomorphic iff ex f being monotone Function of S,T ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) )
proof
let S, T be non empty Poset; ::_thesis: ( S,T are_isomorphic iff ex f being monotone Function of S,T ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) )
hereby  ::_thesis: ( ex f being monotone Function of S,T ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) implies S,T are_isomorphic )
assume  S,T are_isomorphic ; ::_thesis: ex f being monotone Function of S,T ex g being monotone Function of T,S st
( f * g = id T & g * f = id S )
then consider f being Function of S,T such that
A1: f is isomorphic by WAYBEL_1:def_8;
reconsider f = f as monotone Function of S,T by A1;
consider g being Function of T,S such that
A2: g = f " and
A3: g is monotone by A1, WAYBEL_0:def_38;
take f = f; ::_thesis: ex g being monotone Function of T,S st
( f * g = id T & g * f = id S )
reconsider g = g as monotone Function of T,S by A3;
take g = g; ::_thesis: ( f * g = id T & g * f = id S )
 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; ::_thesis: verum
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 ; ::_thesis: S,T are_isomorphic
take  f ; :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic
A6: f is V7() 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 " by A5, A6, FUNCT_2:30;
hence  f is isomorphic by A6, WAYBEL_0:def_38; ::_thesis: verum
end;

theorem :: YELLOW16:17
for S, T being non empty up-complete 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 non empty up-complete Poset; ::_thesis: ( S,T are_isomorphic implies ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S ) )
assume  S,T are_isomorphic ; ::_thesis: ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S )
then consider f being monotone Function of S,T, g being monotone Function of T,S such that
A1: f * g = id T and
A2: g * f = id S by Th16;
 g is isomorphic by A1, A2, Th15;
then A3: g is sups-preserving by WAYBEL13:20;
 f is isomorphic by A1, A2, Th15;
then A4: f is sups-preserving by WAYBEL13:20;
then A5: f is_an_UPS_retraction_of S,T by A1, A3, Def2;
 g is_an_UPS_retraction_of T,S by A2, A4, A3, Def2;
hence  ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S ) by A5, Def4; ::_thesis: verum
end;

theorem Th18: :: YELLOW16:18
for T, S being non empty Poset
for f being monotone Function of T,S
for g being monotone Function of S,T st f * g = id S holds
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; ::_thesis: for f being monotone Function of T,S
for g being monotone Function of S,T st f * g = id S holds
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 )
let f be monotone Function of T,S; ::_thesis: for g being monotone Function of S,T st f * g = id S holds
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 )
let g be monotone Function of S,T; ::_thesis: ( f * g = id S implies 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 ) )
assume A1: f * g = id S ; ::_thesis: 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 )
set h = g * f;
(g * f) * (g * f) = ((g * f) * g) * f by RELAT_1:36
.= (g * (id S)) * f by A1, RELAT_1:36
.= g * f by FUNCT_2:17 ;
then  g * f is idempotent monotone Function of T,T by QUANTAL1:def_9, YELLOW_2:12;
then reconsider h = g * f 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__::_thesis:_for_x,_y_being_Element_of_S_holds_
(_(_x_<=_y_implies_gg_._x_<=_gg_._y_)_&_(_gg_._x_<=_gg_._y_implies_x_<=_y_)_)
let x, y be Element of S; ::_thesis: ( ( x <= y implies gg . x <= gg . y ) & ( gg . x <= gg . y implies x <= y ) )
 ( 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; ::_thesis: ( gg . x <= gg . y implies x <= y )
 (id S) . x = x by FUNCT_1:18;
then A6: x = f . (g . x) by A1, FUNCT_2:15;
 (id S) . y = y by FUNCT_1:18;
then A7: y = f . (g . y) by A1, FUNCT_2:15;
assume  gg . x <= gg . y ; ::_thesis: x <= y
then  g . x <= g . y by A4, YELLOW_0:59;
hence  x <= y by A6, A7, WAYBEL_1:def_2; ::_thesis: verum
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 ; ::_thesis: ( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
thus  h = g * f ; ::_thesis: ( h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
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 ; ::_thesis: S, Image h are_isomorphic
take  gg ; :: according to WAYBEL_1:def_8 ::_thesis: gg is isomorphic
 gg is V7() by A1, A4, FUNCT_2:23;
hence  gg is isomorphic by A8, A5, WAYBEL_0:66; ::_thesis: verum
end;

theorem Th19: :: YELLOW16:19
for T being non empty up-complete Poset
for S being non empty Poset
for f being Function st f is_an_UPS_retraction_of T,S holds
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 non empty up-complete Poset; ::_thesis: for S being non empty Poset
for f being Function st f is_an_UPS_retraction_of T,S holds
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 )
let S be non empty Poset; ::_thesis: for f being Function st f is_an_UPS_retraction_of T,S holds
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 )
let f be Function; ::_thesis: ( f is_an_UPS_retraction_of T,S implies 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 ) )
assume A1: f is directed-sups-preserving Function of T,S ; :: according to YELLOW16:def_2 ::_thesis: ( for g being directed-sups-preserving Function of S,T holds not f * g = id S or 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 ) )
given g being directed-sups-preserving Function of S,T such that A2: f * g = id S ; ::_thesis: 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 )
reconsider f = 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, Th18;
reconsider h = h as directed-sups-preserving projection Function of T,T by A3, WAYBEL20:28;
take  h ; ::_thesis: ( h is_a_retraction_of T, Image h & S, Image h are_isomorphic )
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 full directed-sups-inheriting SubRelStr of T by Th6;
hence  h is_a_retraction_of T, Image h by A4, A6, Def1; ::_thesis: S, Image h are_isomorphic
thus  S, Image h are_isomorphic by A5; ::_thesis: verum
end;

theorem Th20: :: YELLOW16:20
for L being non empty up-complete Poset
for S being non empty Poset st S is_a_retract_of L holds
S is up-complete
proof
let L be non empty up-complete Poset; ::_thesis: for S being non empty Poset st S is_a_retract_of L holds
S is up-complete
let S be non empty Poset; ::_thesis: ( S is_a_retract_of L implies S is up-complete )
given f being Function of L,S such that A1: f is_a_retraction_of L,S ; :: according to YELLOW16:def_3 ::_thesis: S is up-complete
 S is non empty full directed-sups-inheriting SubRelStr of L by A1, Def1;
hence  S is up-complete by Th5; ::_thesis: verum
end;

theorem Th21: :: YELLOW16:21
for L being non empty complete Poset
for S being non empty Poset st S is_a_retract_of L holds
S is complete
proof
let L be non empty complete Poset; ::_thesis: for S being non empty Poset st S is_a_retract_of L holds
S is complete
let S be non empty Poset; ::_thesis: ( S is_a_retract_of L implies S is complete )
given f being Function of L,S such that A1: f is_a_retraction_of L,S ; :: according to YELLOW16:def_3 ::_thesis: S is complete
reconsider f = f as directed-sups-preserving projection Function of L,L by A1, Th12, Th14;
A2: Image f is complete by YELLOW_2:35;
 RelStr(# the carrier of S, the InternalRel of S #) = Image f by A1, Th13;
hence  S is complete by A2, YELLOW_0:3; ::_thesis: verum
end;

theorem Th22: :: YELLOW16:22
for L being complete continuous LATTICE
for S being non empty Poset st S is_a_retract_of L holds
S is continuous
proof
let L be complete continuous LATTICE; ::_thesis: for S being non empty Poset st S is_a_retract_of L holds
S is continuous
let S be non empty Poset; ::_thesis: ( S is_a_retract_of L implies S is continuous )
given f being Function of L,S such that A1: f is_a_retraction_of L,S ; :: according to YELLOW16:def_3 ::_thesis: S is continuous
reconsider g = f as directed-sups-preserving projection Function of L,L by A1, Th12, Th14;
A2: Image g is continuous LATTICE by WAYBEL15:15;
 Image g = RelStr(# the carrier of S, the InternalRel of S #) by A1, Th13;
hence  S is continuous by A2, YELLOW12:15; ::_thesis: verum
end;

theorem :: YELLOW16:23
for L being non empty up-complete Poset
for S being non empty Poset st S is_an_UPS_retract_of L holds
S is up-complete
proof
let L be non empty up-complete Poset; ::_thesis: for S being non empty Poset st S is_an_UPS_retract_of L holds
S is up-complete
let S be non empty Poset; ::_thesis: ( S is_an_UPS_retract_of L implies S is up-complete )
given f being Function of L,S such that A1: f is_an_UPS_retraction_of L,S ; :: according to YELLOW16:def_4 ::_thesis: S is up-complete
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, Th19;
 h = corestr h by WAYBEL_1:30;
then  Image h is_a_retract_of L by A2, Def3;
then  Image h is up-complete by Th20;
hence  S is up-complete by A3, WAYBEL13:30, WAYBEL_1:6; ::_thesis: verum
end;

theorem :: YELLOW16:24
for L being non empty complete Poset
for S being non empty Poset st S is_an_UPS_retract_of L holds
S is complete
proof
let L be non empty complete Poset; ::_thesis: for S being non empty Poset st S is_an_UPS_retract_of L holds
S is complete
let S be non empty Poset; ::_thesis: ( S is_an_UPS_retract_of L implies S is complete )
given f being Function of L,S such that A1: f is_an_UPS_retraction_of L,S ; :: according to YELLOW16:def_4 ::_thesis: S is complete
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, Th19;
 h = corestr h by WAYBEL_1:30;
then  Image h is_a_retract_of L by A2, Def3;
then  Image h is complete by Th21;
hence  S is complete by A3, WAYBEL20:18, WAYBEL_1:6; ::_thesis: verum
end;

theorem :: YELLOW16:25
for L being complete continuous LATTICE
for S being non empty Poset st S is_an_UPS_retract_of L holds
S is continuous
proof
let L be complete continuous LATTICE; ::_thesis: for S being non empty Poset st S is_an_UPS_retract_of L holds
S is continuous
let S be non empty Poset; ::_thesis: ( S is_an_UPS_retract_of L implies S is continuous )
given f being Function of L,S such that A1: f is_an_UPS_retraction_of L,S ; :: according to YELLOW16:def_4 ::_thesis: S is continuous
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, Th19;
 h = corestr h by WAYBEL_1:30;
then  Image h is_a_retract_of L by A2, Def3;
then  Image h is continuous by Th22;
hence  S is continuous by A3, WAYBEL15:9, WAYBEL_1:6; ::_thesis: verum
end;

theorem Th26: :: YELLOW16:26
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 ; ::_thesis: for S being full SubRelStr of L
for R being SubRelStr of S holds
( R is full iff R is full SubRelStr of L )
let S be full SubRelStr of L; ::_thesis: for R being SubRelStr of S holds
( R is full iff R is full SubRelStr of L )
let R be SubRelStr of S; ::_thesis: ( R is full iff R is full SubRelStr of L )
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  ::_thesis: ( R is full SubRelStr of L implies R is full )
assume  R is full ; ::_thesis: R is full SubRelStr of L
then  the InternalRel of R = the InternalRel of S |_2 the carrier of R by YELLOW_0:def_14
.= ( 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; ::_thesis: verum
end;
assume A2: R is full SubRelStr of L ; ::_thesis: R is full
( 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; :: according to YELLOW_0:def_14 ::_thesis: verum
end;

theorem :: YELLOW16:27
for L being non empty transitive RelStr
for S being non empty full directed-sups-inheriting SubRelStr of L
for R being non empty directed-sups-inheriting SubRelStr of S holds R is directed-sups-inheriting SubRelStr of L
proof
let L be non empty transitive RelStr ; ::_thesis: for S being non empty full directed-sups-inheriting SubRelStr of L
for R being non empty directed-sups-inheriting SubRelStr of S holds R is directed-sups-inheriting SubRelStr of L
let S be non empty full directed-sups-inheriting SubRelStr of L; ::_thesis: for R being non empty directed-sups-inheriting SubRelStr of S holds R is directed-sups-inheriting SubRelStr of L
let R be non empty directed-sups-inheriting SubRelStr of S; ::_thesis: R is directed-sups-inheriting SubRelStr of L
reconsider T = R as SubRelStr of L by YELLOW_6:7;
 T is directed-sups-inheriting
proof
let X be directed Subset of T; :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of T )
reconsider Y = X as directed Subset of S by YELLOW_2:7;
assume A1: X <> {} ; ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of T )
assume A2: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of T
then A3: ex_sup_of Y,S by A1, WAYBEL_0:7;
 sup Y = "\/" (X,L) by A1, A2, WAYBEL_0:7;
hence  "\/" (X,L) in the carrier of T by A1, A3, WAYBEL_0:def_4; ::_thesis: verum
end;
hence  R is directed-sups-inheriting SubRelStr of L ; ::_thesis: verum
end;

theorem :: YELLOW16:28
for L being non empty up-complete Poset
for S1, S2 being non empty full directed-sups-inheriting SubRelStr of L st S1 is SubRelStr of S2 holds
S1 is full directed-sups-inheriting SubRelStr of S2
proof
let L be non empty up-complete Poset; ::_thesis: for S1, S2 being non empty full directed-sups-inheriting SubRelStr of L st S1 is SubRelStr of S2 holds
S1 is full directed-sups-inheriting SubRelStr of S2
let S1, S2 be non empty full directed-sups-inheriting SubRelStr of L; ::_thesis: ( S1 is SubRelStr of S2 implies S1 is full directed-sups-inheriting SubRelStr of S2 )
assume  S1 is SubRelStr of S2 ; ::_thesis: S1 is full directed-sups-inheriting SubRelStr of S2
then reconsider S = S1 as SubRelStr of S2 ;
 S is directed-sups-inheriting
proof
let X be directed Subset of S; :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,S2 or "\/" (X,S2) in the carrier of S )
assume  X <> {} ; ::_thesis: ( not ex_sup_of X,S2 or "\/" (X,S2) in the carrier of S )
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  ( not ex_sup_of X,S2 or "\/" (X,S2) in the carrier of S ) by A2; ::_thesis: verum
end;
hence  S1 is full directed-sups-inheriting SubRelStr of S2 by Th26; ::_thesis: verum
end;

begin

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

:: deftheorem Def5 defines Poset-yielding YELLOW16:def_5_:_
 for R being Relation holds
( R is Poset-yielding iff for x being set st x in rng R holds
x is Poset );

registration
cluster Relation-like Poset-yielding  ->  RelStr-yielding reflexive-yielding for set ;
coherence
 for b1 being Relation st b1 is Poset-yielding holds
( b1 is RelStr-yielding & b1 is reflexive-yielding )
proof
let R be Relation; ::_thesis: ( R is Poset-yielding implies ( R is RelStr-yielding & R is reflexive-yielding ) )
assume A1: for x being set st x in rng R holds
x is Poset ; :: according to YELLOW16:def_5 ::_thesis: ( R is RelStr-yielding & R is reflexive-yielding )
hence  for x being set st x in rng R holds
x is RelStr ; :: according to YELLOW_1:def_3 ::_thesis: R is reflexive-yielding
thus  for S being RelStr st S in rng R holds
S is reflexive by A1; :: according to WAYBEL_3:def_8 ::_thesis: verum
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);
:: original: pi
redefine func pi (Y,i) ->  Subset of L;
coherence
 pi (Y,i) is Subset of L
proof
reconsider Y9 = Y as Subset of (product (X --> L)) ;
 pi (Y9,i) is Subset of ((X --> L) . i) ;
hence  pi (Y,i) is Subset of L by FUNCOP_1:7; ::_thesis: verum
end;
end;

registration
let X be set ;
let S be Poset;
clusterX --> S ->  Poset-yielding ;
coherence
 X --> S is Poset-yielding
proof
let x be set ; :: according to YELLOW16:def_5 ::_thesis: ( x in rng (X --> S) implies x is Poset )
assume  x in rng (X --> S) ; ::_thesis: x is Poset
hence  x is Poset by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V24(I) non-Empty Poset-yielding for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is Poset-yielding & b1 is non-Empty )
proof
set P = the non empty Poset;
take  I --> the non empty Poset ; ::_thesis: ( I --> the non empty Poset is Poset-yielding & I --> the non empty Poset is non-Empty )
thus  ( I --> the non empty Poset is Poset-yielding & I --> the non empty Poset is non-Empty ) ; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let J be non-Empty Poset-yielding ManySortedSet of I;
cluster product J ->  transitive antisymmetric ;
coherence
 ( product J is transitive & product J is antisymmetric )
proof
A1: now__::_thesis:_for_i_being_Element_of_I_holds_J_._i_is_Poset
let i be Element of I; ::_thesis: J . i is Poset
 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; ::_thesis: verum
end;
then  for i being Element of I holds J . i is transitive ;
hence  product J is transitive by WAYBEL_3:29; ::_thesis: product J is antisymmetric
 for i being Element of I holds J . i is antisymmetric by A1;
hence  product J is antisymmetric by WAYBEL_3:30; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let J be non-Empty Poset-yielding ManySortedSet of I;
let i be Element of I;
:: original: .
redefine funcJ . i ->  non empty Poset;
coherence
 J . i is non empty Poset
proof
 dom J = I by PARTFUN1:def_2;
then  J . i in rng J by FUNCT_1:def_3;
hence  J . i is non empty Poset by Def5; ::_thesis: verum
end;
end;

Lm1: now__::_thesis:_for_I_being_non_empty_set_
for_J_being_non-Empty_Poset-yielding_ManySortedSet_of_I
for_X_being_Subset_of_(product_J)_st_(_for_i_being_Element_of_I_holds_ex_sup_of_pi_(X,i),J_._i_)_holds_
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_)_)
let I be non empty set ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds
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 ) )
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds
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 ) )
let X be Subset of (product J); ::_thesis: ( ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) implies 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 ) ) )
deffunc H1( Element of I) ->  Element of the carrier of (J . $1) = sup (pi (X,$1));
consider f being ManySortedSet of I such that
A1: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A2: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
 f . i = sup (pi (X,i)) by A1;
hence  f . i is Element of (J . i) ; ::_thesis: verum
end;
 dom f = I by PARTFUN1:def_2;
then reconsider f = 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 ; ::_thesis: 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 ) )
take f = f; ::_thesis: ( ( 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 ) )
thus  for i being Element of I holds f . i = sup (pi (X,i)) by A1; ::_thesis: ( f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) )
thus  f is_>=_than X ::_thesis: for g being Element of (product J) st X is_<=_than g holds
f <= g
proof
let x be Element of (product J); :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= f )
assume A4: x in X ; ::_thesis: x <= f
now__::_thesis:_for_i_being_Element_of_I_holds_x_._i_<=_f_._i
let i be Element of I; ::_thesis: x . i <= f . 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, LATTICE3:def_9; ::_thesis: verum
end;
hence  x <= f by WAYBEL_3:28; ::_thesis: verum
end;
let g be Element of (product J); ::_thesis: ( X is_<=_than g implies f <= g )
assume A7: X is_<=_than g ; ::_thesis: f <= g
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_g_._i
let i be Element of I; ::_thesis: f . i <= g . 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); :: according to LATTICE3:def_9 ::_thesis: ( not a in pi (X,i) or a <= g . i )
assume  a in pi (X,i) ; ::_thesis: a <= g . i
then consider h being Function such that
A10: h in X and
A11: a = h . i by CARD_3:def_6;
reconsider h = h as Element of (product J) by A10;
 h <= g by A7, A10, LATTICE3:def_9;
hence  a <= g . i by A11, WAYBEL_3:28; ::_thesis: verum
end;
 f . i = sup (pi (X,i)) by A1;
hence  f . i <= g . i by A8, A9, YELLOW_0:30; ::_thesis: verum
end;
hence  f <= g by WAYBEL_3:28; ::_thesis: verum
end;

Lm2: now__::_thesis:_for_I_being_non_empty_set_
for_J_being_non-Empty_Poset-yielding_ManySortedSet_of_I
for_X_being_Subset_of_(product_J)_st_(_for_i_being_Element_of_I_holds_ex_inf_of_pi_(X,i),J_._i_)_holds_
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_)_)
let I be non empty set ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds
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 ) )
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds
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 ) )
let X be Subset of (product J); ::_thesis: ( ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) implies 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 ) ) )
deffunc H1( Element of I) ->  Element of the carrier of (J . $1) = inf (pi (X,$1));
consider f being ManySortedSet of I such that
A1: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A2: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
 f . i = inf (pi (X,i)) by A1;
hence  f . i is Element of (J . i) ; ::_thesis: verum
end;
 dom f = I by PARTFUN1:def_2;
then reconsider f = 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 ; ::_thesis: 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 ) )
take f = f; ::_thesis: ( ( 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 ) )
thus  for i being Element of I holds f . i = inf (pi (X,i)) by A1; ::_thesis: ( f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )
thus  f is_<=_than X ::_thesis: for g being Element of (product J) st X is_>=_than g holds
f >= g
proof
let x be Element of (product J); :: according to LATTICE3:def_8 ::_thesis: ( not x in X or f <= x )
assume A4: x in X ; ::_thesis: f <= x
now__::_thesis:_for_i_being_Element_of_I_holds_x_._i_>=_f_._i
let i be Element of I; ::_thesis: x . i >= f . 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, LATTICE3:def_8; ::_thesis: verum
end;
hence  f <= x by WAYBEL_3:28; ::_thesis: verum
end;
let g be Element of (product J); ::_thesis: ( X is_>=_than g implies f >= g )
assume A7: X is_>=_than g ; ::_thesis: f >= g
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_g_._i
let i be Element of I; ::_thesis: f . i >= g . 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); :: according to LATTICE3:def_8 ::_thesis: ( not a in pi (X,i) or g . i <= a )
assume  a in pi (X,i) ; ::_thesis: g . i <= a
then consider h being Function such that
A10: h in X and
A11: a = h . i by CARD_3:def_6;
reconsider h = h as Element of (product J) by A10;
 h >= g by A7, A10, LATTICE3:def_8;
hence  a >= g . i by A11, WAYBEL_3:28; ::_thesis: verum
end;
 f . i = inf (pi (X,i)) by A1;
hence  f . i >= g . i by A8, A9, YELLOW_0:31; ::_thesis: verum
end;
hence  f >= g by WAYBEL_3:28; ::_thesis: verum
end;

theorem Th29: :: YELLOW16:29
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for f being Element of (product J)
for 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 ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I
for f being Element of (product J)
for 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) )
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: for f being Element of (product J)
for 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) )
let f be Element of (product J); ::_thesis: for 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) )
let X be Subset of (product J); ::_thesis: ( f is_>=_than X iff for i being Element of I holds f . i is_>=_than pi (X,i) )
hereby  ::_thesis: ( ( for i being Element of I holds f . i is_>=_than pi (X,i) ) implies f is_>=_than X )
assume A1: f is_>=_than X ; ::_thesis: for i being Element of I holds f . i is_>=_than pi (X,i)
let i be Element of I; ::_thesis: f . i is_>=_than pi (X,i)
thus  f . i is_>=_than pi (X,i) ::_thesis: verum
proof
let x be Element of (J . i); :: according to LATTICE3:def_9 ::_thesis: ( not x in pi (X,i) or x <= f . i )
assume  x in pi (X,i) ; ::_thesis: x <= f . i
then consider g being Function such that
A2: g in X and
A3: x = g . i by CARD_3:def_6;
reconsider g = g as Element of (product J) by A2;
 g <= f by A1, A2, LATTICE3:def_9;
hence  x <= f . i by A3, WAYBEL_3:28; ::_thesis: verum
end;
end;
assume A4: for i being Element of I holds f . i is_>=_than pi (X,i) ; ::_thesis: f is_>=_than X
let g be Element of (product J); :: according to LATTICE3:def_9 ::_thesis: ( not g in X or g <= f )
assume A5: g in X ; ::_thesis: g <= f
now__::_thesis:_for_i_being_Element_of_I_holds_g_._i_<=_f_._i
let i be Element of I; ::_thesis: g . i <= f . 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, LATTICE3:def_9; ::_thesis: verum
end;
hence  g <= f by WAYBEL_3:28; ::_thesis: verum
end;

theorem Th30: :: YELLOW16:30
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for f being Element of (product J)
for 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 ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I
for f being Element of (product J)
for 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) )
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: for f being Element of (product J)
for 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) )
let f be Element of (product J); ::_thesis: for 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) )
let X be Subset of (product J); ::_thesis: ( f is_<=_than X iff for i being Element of I holds f . i is_<=_than pi (X,i) )
hereby  ::_thesis: ( ( for i being Element of I holds f . i is_<=_than pi (X,i) ) implies f is_<=_than X )
assume A1: f is_<=_than X ; ::_thesis: for i being Element of I holds f . i is_<=_than pi (X,i)
let i be Element of I; ::_thesis: f . i is_<=_than pi (X,i)
thus  f . i is_<=_than pi (X,i) ::_thesis: verum
proof
let x be Element of (J . i); :: according to LATTICE3:def_8 ::_thesis: ( not x in pi (X,i) or f . i <= x )
assume  x in pi (X,i) ; ::_thesis: f . i <= x
then consider g being Function such that
A2: g in X and
A3: x = g . i by CARD_3:def_6;
reconsider g = g as Element of (product J) by A2;
 g >= f by A1, A2, LATTICE3:def_8;
hence  f . i <= x by A3, WAYBEL_3:28; ::_thesis: verum
end;
end;
assume A4: for i being Element of I holds f . i is_<=_than pi (X,i) ; ::_thesis: f is_<=_than X
let g be Element of (product J); :: according to LATTICE3:def_8 ::_thesis: ( not g in X or f <= g )
assume A5: g in X ; ::_thesis: f <= g
now__::_thesis:_for_i_being_Element_of_I_holds_g_._i_>=_f_._i
let i be Element of I; ::_thesis: g . i >= f . 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, LATTICE3:def_8; ::_thesis: verum
end;
hence  f <= g by WAYBEL_3:28; ::_thesis: verum
end;

theorem Th31: :: YELLOW16:31
for I being non empty set
for J being non-Empty Poset-yielding 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 ; ::_thesis: for J being non-Empty Poset-yielding 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 )
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: 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 )
let X be Subset of (product J); ::_thesis: ( ex_sup_of X, product J iff for i being Element of I holds ex_sup_of pi (X,i),J . i )
hereby  ::_thesis: ( ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) implies ex_sup_of X, product J )
set f = sup X;
assume A1: ex_sup_of X, product J ; ::_thesis: for i being Element of I holds ex_sup_of pi (X,i),J . i
let i be Element of I; ::_thesis: ex_sup_of pi (X,i),J . i
A2: now__::_thesis:_for_x_being_Element_of_(J_._i)_st_pi_(X,i)_is_<=_than_x_holds_
(sup_X)_._i_<=_x
let x be Element of (J . i); ::_thesis: ( pi (X,i) is_<=_than x implies (sup X) . i <= x )
assume A3: pi (X,i) is_<=_than x ; ::_thesis: (sup X) . i <= x
set g = (sup X) +* (i,x);
A4: dom ((sup X) +* (i,x)) = dom (sup X) by FUNCT_7:30;
 dom (sup X) = I by WAYBEL_3:27;
then A5: ((sup X) +* (i,x)) . i = x by FUNCT_7:31;
now__::_thesis:_for_j_being_Element_of_I_holds_((sup_X)_+*_(i,x))_._j_is_Element_of_(J_._j)
let j be Element of I; ::_thesis: ((sup X) +* (i,x)) . j is Element of (J . j)
 ( ((sup X) +* (i,x)) . j = (sup X) . j or ( ((sup X) +* (i,x)) . j = x & j = i ) ) by A5, FUNCT_7:32;
hence  ((sup X) +* (i,x)) . j is Element of (J . j) ; ::_thesis: verum
end;
then reconsider g = (sup X) +* (i,x) as Element of (product J) by A4, WAYBEL_3:27;
A6: X is_<=_than sup X by A1, YELLOW_0:30;
 X is_<=_than g
proof
let h be Element of (product J); :: according to LATTICE3:def_9 ::_thesis: ( not h in X or h <= g )
assume A7: h in X ; ::_thesis: h <= g
then A8: h . i in pi (X,i) by CARD_3:def_6;
A9: h <= sup X by A6, A7, LATTICE3:def_9;
now__::_thesis:_for_j_being_Element_of_I_holds_h_._j_<=_g_._j
let j be Element of I; ::_thesis: h . j <= g . j
 ( g . j = (sup X) . j or ( g . j = x & j = i ) ) by A5, FUNCT_7:32;
hence  h . j <= g . j by A3, A9, A8, LATTICE3:def_9, WAYBEL_3:28; ::_thesis: verum
end;
hence  h <= g by WAYBEL_3:28; ::_thesis: verum
end;
then  sup X <= g by A1, YELLOW_0:30;
hence  (sup X) . i <= x by A5, WAYBEL_3:28; ::_thesis: verum
end;
 sup X is_>=_than X by A1, YELLOW_0:30;
then  (sup X) . i is_>=_than pi (X,i) by Th29;
hence  ex_sup_of pi (X,i),J . i by A2, YELLOW_0:30; ::_thesis: verum
end;
assume  for i being Element of I holds ex_sup_of pi (X,i),J . i ; ::_thesis: ex_sup_of X, product J
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  ex_sup_of X, product J by YELLOW_0:30; ::_thesis: verum
end;

theorem Th32: :: YELLOW16:32
for I being non empty set
for J being non-Empty Poset-yielding 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 ; ::_thesis: for J being non-Empty Poset-yielding 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 )
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: 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 )
let X be Subset of (product J); ::_thesis: ( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi (X,i),J . i )
hereby  ::_thesis: ( ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) implies ex_inf_of X, product J )
set f = inf X;
assume A1: ex_inf_of X, product J ; ::_thesis: for i being Element of I holds ex_inf_of pi (X,i),J . i
let i be Element of I; ::_thesis: ex_inf_of pi (X,i),J . i
A2: inf X is_<=_than X by A1, YELLOW_0:31;
A3: now__::_thesis:_for_x_being_Element_of_(J_._i)_st_pi_(X,i)_is_>=_than_x_holds_
(inf_X)_._i_>=_x
let x be Element of (J . i); ::_thesis: ( pi (X,i) is_>=_than x implies (inf X) . i >= x )
set g = (inf X) +* (i,x);
A4: dom ((inf X) +* (i,x)) = dom (inf X) by FUNCT_7:30;
 dom (inf X) = I by WAYBEL_3:27;
then A5: ((inf X) +* (i,x)) . i = x by FUNCT_7:31;
now__::_thesis:_for_j_being_Element_of_I_holds_((inf_X)_+*_(i,x))_._j_is_Element_of_(J_._j)
let j be Element of I; ::_thesis: ((inf X) +* (i,x)) . j is Element of (J . j)
 ( ((inf X) +* (i,x)) . j = (inf X) . j or ( ((inf X) +* (i,x)) . j = x & j = i ) ) by A5, FUNCT_7:32;
hence  ((inf X) +* (i,x)) . j is Element of (J . j) ; ::_thesis: verum
end;
then reconsider g = (inf X) +* (i,x) as Element of (product J) by A4, WAYBEL_3:27;
assume A6: pi (X,i) is_>=_than x ; ::_thesis: (inf X) . i >= x
 X is_>=_than g
proof
let h be Element of (product J); :: according to LATTICE3:def_8 ::_thesis: ( not h in X or g <= h )
assume A7: h in X ; ::_thesis: g <= h
then A8: h . i in pi (X,i) by CARD_3:def_6;
A9: h >= inf X by A2, A7, LATTICE3:def_8;
now__::_thesis:_for_j_being_Element_of_I_holds_h_._j_>=_g_._j
let j be Element of I; ::_thesis: h . j >= g . j
 ( g . j = (inf X) . j or ( g . j = x & j = i ) ) by A5, FUNCT_7:32;
hence  h . j >= g . j by A6, A9, A8, LATTICE3:def_8, WAYBEL_3:28; ::_thesis: verum
end;
hence  g <= h by WAYBEL_3:28; ::_thesis: verum
end;
then  inf X >= g by A1, YELLOW_0:31;
hence  (inf X) . i >= x by A5, WAYBEL_3:28; ::_thesis: verum
end;
 (inf X) . i is_<=_than pi (X,i) by A2, Th30;
hence  ex_inf_of pi (X,i),J . i by A3, YELLOW_0:31; ::_thesis: verum
end;
assume  for i being Element of I holds ex_inf_of pi (X,i),J . i ; ::_thesis: ex_inf_of X, product J
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  ex_inf_of X, product J by YELLOW_0:31; ::_thesis: verum
end;

theorem Th33: :: YELLOW16:33
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ex_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi (X,i))
proof
let I be non empty set ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ex_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi (X,i))
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: for X being Subset of (product J) st ex_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi (X,i))
let X be Subset of (product J); ::_thesis: ( ex_sup_of X, product J implies for i being Element of I holds (sup X) . i = sup (pi (X,i)) )
assume  ex_sup_of X, product J ; ::_thesis: for i being Element of I holds (sup X) . i = sup (pi (X,i))
then  for i being Element of I holds ex_sup_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 = 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  for i being Element of I holds (sup X) . i = sup (pi (X,i)) by A1; ::_thesis: verum
end;

theorem Th34: :: YELLOW16:34
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ex_inf_of X, product J holds
for i being Element of I holds (inf X) . i = inf (pi (X,i))
proof
let I be non empty set ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ex_inf_of X, product J holds
for i being Element of I holds (inf X) . i = inf (pi (X,i))
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: for X being Subset of (product J) st ex_inf_of X, product J holds
for i being Element of I holds (inf X) . i = inf (pi (X,i))
let X be Subset of (product J); ::_thesis: ( ex_inf_of X, product J implies for i being Element of I holds (inf X) . i = inf (pi (X,i)) )
assume  ex_inf_of X, product J ; ::_thesis: for i being Element of I holds (inf X) . i = inf (pi (X,i))
then  for i being Element of I holds ex_inf_of pi (X,i),J . i by Th32;
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  for i being Element of I holds (inf X) . i = inf (pi (X,i)) by A1; ::_thesis: verum
end;

theorem Th35: :: YELLOW16:35
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 ; ::_thesis: 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
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: for X being directed Subset of (product J)
for i being Element of I holds pi (X,i) is directed
let X be directed Subset of (product J); ::_thesis: for i being Element of I holds pi (X,i) is directed
let i be Element of I; ::_thesis: pi (X,i) is directed
let x, y be Element of (J . i); :: according to WAYBEL_0:def_1 ::_thesis: ( not x in pi (X,i) or not y in pi (X,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (X,i) & x <= b1 & y <= b1 ) )
assume  x in pi (X,i) ; ::_thesis: ( not y in pi (X,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (X,i) & x <= b1 & y <= b1 ) )
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) ; ::_thesis: ex b1 being Element of the carrier of (J . i) st
( b1 in pi (X,i) & x <= b1 & y <= b1 )
then consider g being Function such that
A3: g in X and
A4: y = g . i by CARD_3:def_6;
reconsider f = f, g = 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 ; ::_thesis: ( h . i in pi (X,i) & x <= h . i & y <= h . i )
thus  h . i in pi (X,i) by A5, CARD_3:def_6; ::_thesis: ( x <= h . i & y <= h . i )
thus  ( x <= h . i & y <= h . i ) by A2, A4, A6, A7, WAYBEL_3:28; ::_thesis: verum
end;

theorem Th36: :: YELLOW16:36
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 ; ::_thesis: 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
let J, K be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds K . i is SubRelStr of J . i ) implies product K is SubRelStr of product J )
assume A1: for i being Element of I holds K . i is SubRelStr of J . i ; ::_thesis: product K is SubRelStr of product J
A2: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(Carrier_K)_._i_c=_(Carrier_J)_._i
let i be set ; ::_thesis: ( i in I implies (Carrier K) . i c= (Carrier J) . i )
assume  i in I ; ::_thesis: (Carrier K) . i c= (Carrier J) . 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_13;
A4: ex R being 1-sorted st
( R = K . j & (Carrier K) . j = the carrier of R ) by PRALG_1:def_13;
 K . j is SubRelStr of J . j by A1;
hence  (Carrier K) . i c= (Carrier J) . i by A3, A4, YELLOW_0:def_13; ::_thesis: verum
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; :: according to YELLOW_0:def_13 ::_thesis: the InternalRel of (product K) c= the InternalRel of (product J)
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of (product K) or [x,y] in the InternalRel of (product J) )
assume A9: [x,y] in the InternalRel of (product K) ; ::_thesis: [x,y] in the InternalRel of (product J)
then A10: x in the carrier of (product K) by ZFMISC_1:87;
A11: y in the carrier of (product K) by A9, ZFMISC_1:87;
reconsider x = x, y = y as Element of (product K) by A9, ZFMISC_1:87;
reconsider f = x, g = y as Element of (product J) by A8, A10, A11;
A12: x <= y by A9, ORDERS_2:def_5;
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_g_._i
let i be Element of I; ::_thesis: f . i <= g . i
A13: x . i <= y . i by A12, WAYBEL_3:28;
 K . i is SubRelStr of J . i by A1;
hence  f . i <= g . i by A13, YELLOW_0:59; ::_thesis: verum
end;
then  f <= g by WAYBEL_3:28;
hence  [x,y] in the InternalRel of (product J) by ORDERS_2:def_5; ::_thesis: verum
end;

theorem Th37: :: YELLOW16:37
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 ; ::_thesis: 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
let J, K be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds K . i is full SubRelStr of J . i ) implies product K is full SubRelStr of product J )
assume A1: for i being Element of I holds K . i is full SubRelStr of J . i ; ::_thesis: product K is full SubRelStr of product J
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 Th36;
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; :: according to YELLOW_0:def_14,XBOOLE_0:def_10 ::_thesis: K43( the InternalRel of (product J), the carrier of S) c= the InternalRel of S
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in K43( the InternalRel of (product J), the carrier of S) or [x,y] in the InternalRel of S )
assume A3: [x,y] in the InternalRel of (product J) |_2 the carrier of S ; ::_thesis: [x,y] in the InternalRel 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 = x, y = 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 = x, y = y as Element of (product K) ;
A5: a <= b by A4, ORDERS_2:def_5;
now__::_thesis:_for_i_being_Element_of_I_holds_x_._i_<=_y_._i
let i be Element of I; ::_thesis: x . i <= y . 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; ::_thesis: verum
end;
then  x <= y by WAYBEL_3:28;
hence  [x,y] in the InternalRel of S by ORDERS_2:def_5; ::_thesis: verum
end;
hence  product K is full SubRelStr of product J ; ::_thesis: verum
end;

theorem :: YELLOW16:38
for L being non empty RelStr
for S being non empty SubRelStr of L
for X being set holds S |^ X is SubRelStr of L |^ X
proof
let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L
for X being set holds S |^ X is SubRelStr of L |^ X
let S be non empty SubRelStr of L; ::_thesis: for X being set holds S |^ X is SubRelStr of L |^ X
let X be set ; ::_thesis: S |^ X is SubRelStr of L |^ X
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: S |^ X is SubRelStr of L |^ X
then A2: L |^ X = RelStr(# {{}},(id {{}}) #) by YELLOW_1:27;
 S |^ X = RelStr(# {{}},(id {{}}) #) by A1, YELLOW_1:27;
hence  S |^ X is SubRelStr of L |^ X by A2, YELLOW_6:6; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: S |^ X is SubRelStr of L |^ X
then reconsider X = X as non empty set ;
now__::_thesis:_for_i_being_Element_of_X_holds_(X_-->_S)_._i_is_SubRelStr_of_(X_-->_L)_._i
let i be Element of X; ::_thesis: (X --> S) . i is SubRelStr of (X --> L) . i
 (X --> L) . i = L by FUNCOP_1:7;
hence  (X --> S) . i is SubRelStr of (X --> L) . i by FUNCOP_1:7; ::_thesis: verum
end;
hence  S |^ X is SubRelStr of L |^ X by Th36; ::_thesis: verum
end;
end;
end;

theorem Th39: :: YELLOW16:39
for L being non empty RelStr
for S being non empty full SubRelStr of L
for X being set holds S |^ X is full SubRelStr of L |^ X
proof
let L be non empty RelStr ; ::_thesis: for S being non empty full SubRelStr of L
for X being set holds S |^ X is full SubRelStr of L |^ X
let S be non empty full SubRelStr of L; ::_thesis: for X being set holds S |^ X is full SubRelStr of L |^ X
let X be set ; ::_thesis: S |^ X is full SubRelStr of L |^ X
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: S |^ X is full SubRelStr of L |^ X
then A2: L |^ X = RelStr(# {{}},(id {{}}) #) by YELLOW_1:27;
 S |^ X = RelStr(# {{}},(id {{}}) #) by A1, YELLOW_1:27;
hence  S |^ X is full SubRelStr of L |^ X by A2, YELLOW_6:6; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: S |^ X is full SubRelStr of L |^ X
then reconsider X = X as non empty set ;
now__::_thesis:_for_i_being_Element_of_X_holds_(X_-->_S)_._i_is_full_SubRelStr_of_(X_-->_L)_._i
let i be Element of X; ::_thesis: (X --> S) . i is full SubRelStr of (X --> L) . i
 (X --> L) . i = L by FUNCOP_1:7;
hence  (X --> S) . i is full SubRelStr of (X --> L) . i by FUNCOP_1:7; ::_thesis: verum
end;
hence  S |^ X is full SubRelStr of L |^ X by Th37; ::_thesis: verum
end;
end;
end;

begin

definition
let S, T be non empty RelStr ;
let X be set ;
predS inherits_sup_of X,T means :Def6: :: YELLOW16:def 6
( ex_sup_of X,T implies "\/" (X,T) in the carrier of S );
predS inherits_inf_of X,T means :Def7: :: YELLOW16:def 7
( ex_inf_of X,T implies "/\" (X,T) in the carrier of S );
end;

:: deftheorem Def6 defines inherits_sup_of YELLOW16:def_6_:_
 for S, T being non empty RelStr
for X being set holds
( S inherits_sup_of X,T iff ( ex_sup_of X,T implies "\/" (X,T) in the carrier of S ) );

:: deftheorem Def7 defines inherits_inf_of YELLOW16:def_7_:_
 for S, T being non empty RelStr
for X being set holds
( S inherits_inf_of X,T iff ( ex_inf_of X,T implies "/\" (X,T) in the carrier of S ) );

theorem Th40: :: YELLOW16:40
for T being non empty transitive RelStr
for S being non empty full 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) ) ) )
proof
let T be non empty transitive RelStr ; ::_thesis: for S being non empty full 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) ) ) )
let S be non empty full SubRelStr of T; ::_thesis: 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) ) ) )
let X be Subset of S; ::_thesis: ( S inherits_sup_of X,T iff ( ex_sup_of X,T implies ( ex_sup_of X,S & sup X = "\/" (X,T) ) ) )
hereby  ::_thesis: ( ( ex_sup_of X,T implies ( ex_sup_of X,S & sup X = "\/" (X,T) ) ) implies S inherits_sup_of X,T )
assume that
A1: S inherits_sup_of X,T and
A2: ex_sup_of X,T ; ::_thesis: ( ex_sup_of X,S & sup X = "\/" (X,T) )
 "\/" (X,T) in the carrier of S by A1, A2, Def6;
hence  ( ex_sup_of X,S & sup X = "\/" (X,T) ) by A2, YELLOW_0:64; ::_thesis: verum
end;
assume A3: ( ex_sup_of X,T implies ( ex_sup_of X,S & sup X = "\/" (X,T) ) ) ; ::_thesis: S inherits_sup_of X,T
assume  ex_sup_of X,T ; :: according to YELLOW16:def_6 ::_thesis: "\/" (X,T) in the carrier of S
hence  "\/" (X,T) in the carrier of S by A3; ::_thesis: verum
end;

theorem :: YELLOW16:41
for T being non empty transitive RelStr
for S being non empty full 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) ) ) )
proof
let T be non empty transitive RelStr ; ::_thesis: for S being non empty full 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) ) ) )
let S be non empty full SubRelStr of T; ::_thesis: 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) ) ) )
let X be Subset of S; ::_thesis: ( S inherits_inf_of X,T iff ( ex_inf_of X,T implies ( ex_inf_of X,S & inf X = "/\" (X,T) ) ) )
hereby  ::_thesis: ( ( ex_inf_of X,T implies ( ex_inf_of X,S & inf X = "/\" (X,T) ) ) implies S inherits_inf_of X,T )
assume that
A1: S inherits_inf_of X,T and
A2: ex_inf_of X,T ; ::_thesis: ( ex_inf_of X,S & inf X = "/\" (X,T) )
 "/\" (X,T) in the carrier of S by A1, A2, Def7;
hence  ( ex_inf_of X,S & inf X = "/\" (X,T) ) by A2, YELLOW_0:63; ::_thesis: verum
end;
assume A3: ( ex_inf_of X,T implies ( ex_inf_of X,S & inf X = "/\" (X,T) ) ) ; ::_thesis: S inherits_inf_of X,T
assume  ex_inf_of X,T ; :: according to YELLOW16:def_7 ::_thesis: "/\" (X,T) in the carrier of S
hence  "/\" (X,T) in the carrier of S by A3; ::_thesis: verum
end;

scheme :: YELLOW16:sch 1
ProductSupsInheriting{ F1() ->  non empty set , F2() ->  non-Empty Poset-yielding ManySortedSet of F1(), F3() ->  non-Empty Poset-yielding ManySortedSet of F1(), P1[ set , set ] } :
 for X being Subset of (product F3()) st P1[X, product F3()] holds
product F3() inherits_sup_of X, product F2()
provided
A1: for X being Subset of (product F3()) st P1[X, product F3()] holds
for i being Element of F1() holds P1[ pi (X,i),F3() . i] and
A2: for i being Element of F1() holds F3() . i is full SubRelStr of F2() . i and
A3: for i being Element of F1()
for X being Subset of (F3() . i) st P1[X,F3() . i] holds
F3() . i inherits_sup_of X,F2() . i
proof
let X be Subset of (product F3()); ::_thesis: ( P1[X, product F3()] implies product F3() inherits_sup_of X, product F2() )
assume that
A4: P1[X, product F3()] and
A5: ex_sup_of X, product F2() ; :: according to YELLOW16:def_6 ::_thesis: "\/" (X,(product F2())) in the carrier of (product F3())
 product F3() is SubRelStr of product F2() by A2, Th37;
then  the carrier of (product F3()) c= the carrier of (product F2()) by YELLOW_0:def_13;
then reconsider Y = X as Subset of (product F2()) by XBOOLE_1:1;
set f = "\/" (X,(product F2()));
A6: now__::_thesis:_for_i_being_Element_of_F1()_holds_("\/"_(X,(product_F2())))_._i_is_Element_of_(F3()_._i)
let i be Element of F1(); ::_thesis: ("\/" (X,(product F2()))) . i is Element of (F3() . i)
A7: ex_sup_of pi (Y,i),F2() . i by A5, Th31;
 F3() . i inherits_sup_of pi (X,i),F2() . i by A1, A3, A4;
then  sup (pi (Y,i)) in the carrier of (F3() . i) by A7, Def6;
hence  ("\/" (X,(product F2()))) . i is Element of (F3() . i) by A5, Th33; ::_thesis: verum
end;
 dom ("\/" (X,(product F2()))) = F1() by WAYBEL_3:27;
then  "\/" (X,(product F2())) is Element of (product F3()) by A6, WAYBEL_3:27;
hence  "\/" (X,(product F2())) in the carrier of (product F3()) ; ::_thesis: verum
end;

scheme :: YELLOW16:sch 2
PowerSupsInheriting{ F1() ->  non empty set , F2() ->  non empty Poset, F3() ->  non empty full SubRelStr of F2(), P1[ set , set ] } :
 for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
F3() |^ F1() inherits_sup_of X,F2() |^ F1()
provided
A1: for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
for i being Element of F1() holds P1[ pi (X,i),F3()] and
A2: for X being Subset of F3() st P1[X,F3()] holds
F3() inherits_sup_of X,F2()
proof
reconsider K = F1() --> F3(), J = F1() --> F2() as non-Empty Poset-yielding ManySortedSet of F1() ;
A3: now__::_thesis:_for_X_being_Subset_of_(product_K)_st_P1[X,_product_K]_holds_
for_i_being_Element_of_F1()_holds_P1[_pi_(X,i),K_._i]
let X be Subset of (product K); ::_thesis: ( P1[X, product K] implies for i being Element of F1() holds P1[ pi (X,i),K . i] )
assume A4: P1[X, product K] ; ::_thesis: for i being Element of F1() holds P1[ pi (X,i),K . i]
let i be Element of F1(); ::_thesis: P1[ pi (X,i),K . i]
 K . i = F3() by FUNCOP_1:7;
hence  P1[ pi (X,i),K . i] by A1, A4; ::_thesis: verum
end;
A5: now__::_thesis:_for_i_being_Element_of_F1()
for_X_being_Subset_of_(K_._i)_st_P1[X,K_._i]_holds_
K_._i_inherits_sup_of_X,J_._i
let i be Element of F1(); ::_thesis: for X being Subset of (K . i) st P1[X,K . i] holds
K . i inherits_sup_of X,J . i
let X be Subset of (K . i); ::_thesis: ( P1[X,K . i] implies K . i inherits_sup_of X,J . i )
assume A6: P1[X,K . i] ; ::_thesis: K . i inherits_sup_of X,J . i
A7: J . i = F2() by FUNCOP_1:7;
 K . i = F3() by FUNCOP_1:7;
hence  K . i inherits_sup_of X,J . i by A2, A6, A7; ::_thesis: verum
end;
A8: now__::_thesis:_for_i_being_Element_of_F1()_holds_K_._i_is_full_SubRelStr_of_J_._i
let i be Element of F1(); ::_thesis: K . i is full SubRelStr of J . i
 J . i = F2() by FUNCOP_1:7;
hence  K . i is full SubRelStr of J . i by FUNCOP_1:7; ::_thesis: verum
end;
 for X being Subset of (product K) st P1[X, product K] holds
product K inherits_sup_of X, product J from YELLOW16:sch_1(A3, A8, A5);
hence  for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
F3() |^ F1() inherits_sup_of X,F2() |^ F1() ; ::_thesis: verum
end;

scheme :: YELLOW16:sch 3
ProductInfsInheriting{ F1() ->  non empty set , F2() ->  non-Empty Poset-yielding ManySortedSet of F1(), F3() ->  non-Empty Poset-yielding ManySortedSet of F1(), P1[ set , set ] } :
 for X being Subset of (product F3()) st P1[X, product F3()] holds
product F3() inherits_inf_of X, product F2()
provided
A1: for X being Subset of (product F3()) st P1[X, product F3()] holds
for i being Element of F1() holds P1[ pi (X,i),F3() . i] and
A2: for i being Element of F1() holds F3() . i is full SubRelStr of F2() . i and
A3: for i being Element of F1()
for X being Subset of (F3() . i) st P1[X,F3() . i] holds
F3() . i inherits_inf_of X,F2() . i
proof
let X be Subset of (product F3()); ::_thesis: ( P1[X, product F3()] implies product F3() inherits_inf_of X, product F2() )
assume that
A4: P1[X, product F3()] and
A5: ex_inf_of X, product F2() ; :: according to YELLOW16:def_7 ::_thesis: "/\" (X,(product F2())) in the carrier of (product F3())
 product F3() is SubRelStr of product F2() by A2, Th37;
then  the carrier of (product F3()) c= the carrier of (product F2()) by YELLOW_0:def_13;
then reconsider Y = X as Subset of (product F2()) by XBOOLE_1:1;
set f = "/\" (X,(product F2()));
A6: now__::_thesis:_for_i_being_Element_of_F1()_holds_("/\"_(X,(product_F2())))_._i_is_Element_of_(F3()_._i)
let i be Element of F1(); ::_thesis: ("/\" (X,(product F2()))) . i is Element of (F3() . i)
A7: ex_inf_of pi (Y,i),F2() . i by A5, Th32;
 F3() . i inherits_inf_of pi (X,i),F2() . i by A1, A3, A4;
then  inf (pi (Y,i)) in the carrier of (F3() . i) by A7, Def7;
hence  ("/\" (X,(product F2()))) . i is Element of (F3() . i) by A5, Th34; ::_thesis: verum
end;
 dom ("/\" (X,(product F2()))) = F1() by WAYBEL_3:27;
then  "/\" (X,(product F2())) is Element of (product F3()) by A6, WAYBEL_3:27;
hence  "/\" (X,(product F2())) in the carrier of (product F3()) ; ::_thesis: verum
end;

scheme :: YELLOW16:sch 4
PowerInfsInheriting{ F1() ->  non empty set , F2() ->  non empty Poset, F3() ->  non empty full SubRelStr of F2(), P1[ set , set ] } :
 for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
F3() |^ F1() inherits_inf_of X,F2() |^ F1()
provided
A1: for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
for i being Element of F1() holds P1[ pi (X,i),F3()] and
A2: for X being Subset of F3() st P1[X,F3()] holds
F3() inherits_inf_of X,F2()
proof
reconsider K = F1() --> F3(), J = F1() --> F2() as non-Empty Poset-yielding ManySortedSet of F1() ;
A3: now__::_thesis:_for_X_being_Subset_of_(product_K)_st_P1[X,_product_K]_holds_
for_i_being_Element_of_F1()_holds_P1[_pi_(X,i),K_._i]
let X be Subset of (product K); ::_thesis: ( P1[X, product K] implies for i being Element of F1() holds P1[ pi (X,i),K . i] )
assume A4: P1[X, product K] ; ::_thesis: for i being Element of F1() holds P1[ pi (X,i),K . i]
let i be Element of F1(); ::_thesis: P1[ pi (X,i),K . i]
 K . i = F3() by FUNCOP_1:7;
hence  P1[ pi (X,i),K . i] by A1, A4; ::_thesis: verum
end;
A5: now__::_thesis:_for_i_being_Element_of_F1()
for_X_being_Subset_of_(K_._i)_st_P1[X,K_._i]_holds_
K_._i_inherits_inf_of_X,J_._i
let i be Element of F1(); ::_thesis: for X being Subset of (K . i) st P1[X,K . i] holds
K . i inherits_inf_of X,J . i
let X be Subset of (K . i); ::_thesis: ( P1[X,K . i] implies K . i inherits_inf_of X,J . i )
assume A6: P1[X,K . i] ; ::_thesis: K . i inherits_inf_of X,J . i
A7: J . i = F2() by FUNCOP_1:7;
 K . i = F3() by FUNCOP_1:7;
hence  K . i inherits_inf_of X,J . i by A2, A6, A7; ::_thesis: verum
end;
A8: now__::_thesis:_for_i_being_Element_of_F1()_holds_K_._i_is_full_SubRelStr_of_J_._i
let i be Element of F1(); ::_thesis: K . i is full SubRelStr of J . i
 J . i = F2() by FUNCOP_1:7;
hence  K . i is full SubRelStr of J . i by FUNCOP_1:7; ::_thesis: verum
end;
 for X being Subset of (product K) st P1[X, product K] holds
product K inherits_inf_of X, product J from YELLOW16:sch_3(A3, A8, A5);
hence  for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
F3() |^ F1() inherits_inf_of X,F2() |^ F1() ; ::_thesis: verum
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
 not pi (X,i) is empty
proof
reconsider Y = X as non empty Subset of (product (I --> L)) ;
set f = the Element of Y;
reconsider f = the Element of Y as Function ;
 f . i in pi (X,i) by CARD_3:def_6;
hence  not pi (X,i) is empty ; ::_thesis: verum
end;
end;

theorem :: YELLOW16:42
for L being non empty Poset
for S being non empty full directed-sups-inheriting SubRelStr of L
for X being non empty set holds S |^ X is directed-sups-inheriting SubRelStr of L |^ X
proof
let L be non empty Poset; ::_thesis: for S being non empty full directed-sups-inheriting SubRelStr of L
for X being non empty set holds S |^ X is directed-sups-inheriting SubRelStr of L |^ X
let S be non empty full directed-sups-inheriting SubRelStr of L; ::_thesis: for X being non empty set holds S |^ X is directed-sups-inheriting SubRelStr of L |^ X
let X be non empty set ; ::_thesis: S |^ X is directed-sups-inheriting SubRelStr of L |^ X
reconsider SX = S |^ X as non empty full SubRelStr of L |^ X by Th39;
defpred S1[ set , non empty reflexive RelStr ] means $1 is non empty directed Subset of $2;
A1: now__::_thesis:_for_A_being_Subset_of_(S_|^_X)_st_S1[A,S_|^_X]_holds_
for_i_being_Element_of_X_holds_S1[_pi_(A,i),S]
let A be Subset of (S |^ X); ::_thesis: ( S1[A,S |^ X] implies for i being Element of X holds S1[ pi (A,i),S] )
assume  S1[A,S |^ X] ; ::_thesis: for i being Element of X holds S1[ pi (A,i),S]
then reconsider B = A as non empty directed Subset of (S |^ X) ;
let i be Element of X; ::_thesis: S1[ pi (A,i),S]
 (X --> S) . i = S by FUNCOP_1:7;
then  pi (B,i) is non empty directed Subset of S by Th35;
hence  S1[ pi (A,i),S] ; ::_thesis: verum
end;
A2: now__::_thesis:_for_X_being_Subset_of_S_st_S1[X,S]_holds_
S_inherits_sup_of_X,L
let X be Subset of S; ::_thesis: ( S1[X,S] implies S inherits_sup_of X,L )
assume  S1[X,S] ; ::_thesis: S inherits_sup_of X,L
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 by Th40; ::_thesis: verum
end;
 SX is directed-sups-inheriting
proof
let A be directed Subset of SX; :: according to WAYBEL_0:def_4 ::_thesis: ( A = {} or not ex_sup_of A,L |^ X or "\/" (A,(L |^ X)) in the carrier of SX )
 for A being Subset of (S |^ X) st S1[A,S |^ X] holds
S |^ X inherits_sup_of A,L |^ X from YELLOW16:sch_2(A1, A2);
then  ( A <> {} implies S |^ X inherits_sup_of A,L |^ X ) ;
hence  ( A = {} or not ex_sup_of A,L |^ X or "\/" (A,(L |^ X)) in the carrier of SX ) by Def6; ::_thesis: verum
end;
hence  S |^ X is directed-sups-inheriting SubRelStr of L |^ X ; ::_thesis: verum
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
 not pi (X,i) is empty
proof
set f = the Element of X;
reconsider f = the Element of X as Function ;
 f . i in pi (X,i) by CARD_3:def_6;
hence  not pi (X,i) is empty ; ::_thesis: verum
end;
end;

theorem Th43: :: YELLOW16:43
for X being non empty set
for L being non empty up-complete Poset holds L |^ X is up-complete
proof
let X be non empty set ; ::_thesis: for L being non empty up-complete Poset holds L |^ X is up-complete
let L be non empty up-complete Poset; ::_thesis: L |^ X is up-complete
now__::_thesis:_for_A_being_non_empty_directed_Subset_of_(L_|^_X)_holds_ex_sup_of_A,L_|^_X
let A be non empty directed Subset of (L |^ X); ::_thesis: ex_sup_of A,L |^ X
reconsider B = A as non empty directed Subset of (product (X --> L)) ;
now__::_thesis:_for_x_being_Element_of_X_holds_ex_sup_of_pi_(A,x),(X_-->_L)_._x
let x be Element of X; ::_thesis: ex_sup_of pi (A,x),(X --> L) . x
A1: (X --> L) . x = L by FUNCOP_1:7;
 ( pi (B,x) is directed & not pi (B,x) is empty ) by Th35;
hence  ex_sup_of pi (A,x),(X --> L) . x by A1, WAYBEL_0:75; ::_thesis: verum
end;
hence  ex_sup_of A,L |^ X by Th31; ::_thesis: verum
end;
hence  L |^ X is up-complete by WAYBEL_0:75; ::_thesis: verum
end;

registration
let L be non empty up-complete Poset;
let X be non empty set ;
clusterL |^ X ->  up-complete ;
coherence
 L |^ X is up-complete by Th43;
end;

begin

theorem Th44: :: YELLOW16:44
for T being non empty TopSpace
for 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; ::_thesis: for 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
let S be non empty SubSpace of T; ::_thesis: for f being Function of T,S st f is being_a_retraction holds
rng f = the carrier of S
let f be Function of T,S; ::_thesis: ( f is being_a_retraction implies rng f = the carrier of S )
assume A1: for W being Point of T st W in the carrier of S holds
f . W = W ; :: according to BORSUK_1:def_16 ::_thesis: rng f = the carrier of S
thus  rng f c= the carrier of S ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of S c= rng f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of S or x in rng f )
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 ; ::_thesis: x in rng f
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  x in rng f by A5, FUNCT_1:def_3; ::_thesis: verum
end;

theorem :: YELLOW16:45
for T being non empty TopSpace
for 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; ::_thesis: for 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
let S be non empty SubSpace of T; ::_thesis: for f being continuous Function of T,S st f is being_a_retraction holds
f is idempotent
A1: [#] S = the carrier of S ;
let f be continuous Function of T,S; ::_thesis: ( f is being_a_retraction implies f is idempotent )
assume A2: f is being_a_retraction ; ::_thesis: f is idempotent
A3: rng f = the carrier of S by A2, Th44;
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__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_T_holds_
(f_*_f)_._x_=_f_._x
let x be set ; ::_thesis: ( x in the carrier of T implies (f * f) . x = f . x )
assume A7: x in the carrier of T ; ::_thesis: (f * f) . x = f . x
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, BORSUK_1:def_16; ::_thesis: verum
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  f is idempotent by QUANTAL1:def_9; ::_thesis: verum
end;

theorem Th46: :: YELLOW16:46
for T being non empty TopSpace
for 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; ::_thesis: for V being open Subset of T holds chi (V, the carrier of T) is continuous Function of T,Sierpinski_Space
let V be open Subset of T; ::_thesis: chi (V, the carrier of T) is continuous Function of T,Sierpinski_Space
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__::_thesis:_for_W_being_Subset_of_Sierpinski_Space_st_W_is_open_holds_
c_"_W_is_open
let W be Subset of Sierpinski_Space; ::_thesis: ( W is open implies c " W is open )
assume  W is open ; ::_thesis: c " 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; ::_thesis: verum
end;
 [#] Sierpinski_Space <> {} ;
hence  chi (V, the carrier of T) is continuous Function of T,Sierpinski_Space by A4, TOPS_2:43; ::_thesis: verum
end;

theorem :: YELLOW16:47
for T being non empty TopSpace
for 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; ::_thesis: for 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
let x, y be Element of T; ::_thesis: ( ( for W being open Subset of T st y in W holds
x in W ) implies (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T )
assume A1: for W being open Subset of T st y in W holds
x in W ; ::_thesis: (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T
A2: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9;
then reconsider i = (0,1) --> (y,x) as Function of Sierpinski_Space,T ;
A3: i . 1 = x by FUNCT_4:63;
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__::_thesis:_for_W_being_Subset_of_T_st_W_is_open_holds_
i_"_W_is_open
let W be Subset of T; ::_thesis: ( W is open implies i " W is open )
assume  W is open ; ::_thesis: i " 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;
 ( i " W = {} or i " W = {0} or i " W = {1} or i " W = {0,1} ) by A2, ZFMISC_1:36;
then  i " W in {{},{1},{0,1}} by A7, A3, A6, A5, A4, A9, ENUMSET1:def_1, FUNCT_2:38;
then  i " W in the topology of Sierpinski_Space by WAYBEL18:def_9;
hence  i " W is open by PRE_TOPC:def_2; ::_thesis: verum
end;
 [#] T <> {} ;
hence  (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T by A8, TOPS_2:43; ::_thesis: verum
end;

theorem :: YELLOW16:48
for T being non empty TopSpace
for 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; ::_thesis: for 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
let x, y be Element of T; ::_thesis: 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
let V be open Subset of T; ::_thesis: ( x in V & not y in V implies (chi (V, the carrier of T)) * ((0,1) --> (y,x)) = id Sierpinski_Space )
assume that
A1: x in V and
A2: not y in V ; ::_thesis: (chi (V, the carrier of T)) * ((0,1) --> (y,x)) = id Sierpinski_Space
reconsider c = chi (V, the carrier of T) as Function of T,Sierpinski_Space by Th46;
A3: c . x = 1 by A1, FUNCT_3:def_3;
A4: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9;
then reconsider i = (0,1) --> (y,x) as Function of Sierpinski_Space,T ;
A5: i . 1 = x by FUNCT_4:63;
A6: c . y = 0 by A2, FUNCT_3:def_3;
A7: i . 0 = y by FUNCT_4:63;
now__::_thesis:_(_c_*_i_is_Function_of_Sierpinski_Space,Sierpinski_Space_&_(_for_a_being_Element_of_Sierpinski_Space_holds_(c_*_i)_._a_=_(id_Sierpinski_Space)_._a_)_)
thus  c * i is Function of Sierpinski_Space,Sierpinski_Space ; ::_thesis: for a being Element of Sierpinski_Space holds (c * i) . a = (id Sierpinski_Space) . a
let a be Element of Sierpinski_Space; ::_thesis: (c * i) . a = (id Sierpinski_Space) . a
 ( a = 0 or a = 1 ) by A4, TARSKI:def_2;
hence (c * i) . a = a by A7, A5, A3, A6, FUNCT_2:15
.= (id Sierpinski_Space) . a by FUNCT_1:18 ;
::_thesis: verum
end;
hence  (chi (V, the carrier of T)) * ((0,1) --> (y,x)) = id Sierpinski_Space by FUNCT_2:63; ::_thesis: verum
end;

theorem :: YELLOW16:49
for T being non empty 1-sorted
for V, W being Subset of T
for S being TopAugmentation of BoolePoset 1
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 ; ::_thesis: for V, W being Subset of T
for S being TopAugmentation of BoolePoset 1
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 )
let V, W be Subset of T; ::_thesis: for S being TopAugmentation of BoolePoset 1
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 )
let S be TopAugmentation of BoolePoset 1; ::_thesis: 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 )
let c1, c2 be Function of T,S; ::_thesis: ( c1 = chi (V, the carrier of T) & c2 = chi (W, the carrier of T) implies ( V c= W iff c1 <= c2 ) )
assume that
A1: c1 = chi (V, the carrier of T) and
A2: c2 = chi (W, the carrier of T) ; ::_thesis: ( V c= W iff c1 <= c2 )
A3: RelStr(# the carrier of S, the InternalRel of S #) = BoolePoset 1 by YELLOW_9:def_4;
hereby  ::_thesis: ( c1 <= c2 implies V c= W )
assume A4: V c= W ; ::_thesis: c1 <= c2
now__::_thesis:_for_z_being_set_st_z_in_the_carrier_of_T_holds_
ex_a,_b_being_Element_of_S_st_
(_a_=_c1_._z_&_b_=_c2_._z_&_a_<=_b_)
let z be set ; ::_thesis: ( z in the carrier of T implies ex a, b being Element of S st
( a = c1 . z & b = c2 . z & a <= b ) )
assume  z in the carrier of T ; ::_thesis: ex a, b being Element of S st
( a = c1 . z & b = c2 . z & a <= b )
then reconsider x = z as Element of T ;
reconsider a = c1 . x, b = c2 . x as Element of (BoolePoset 1) 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 by XBOOLE_1:2;
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; ::_thesis: verum
end;
hence  c1 <= c2 by YELLOW_2:def_1; ::_thesis: verum
end;
assume A5: c1 <= c2 ; ::_thesis: V c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in W )
assume that
A6: x in V and
A7: not x in W ; ::_thesis: contradiction
reconsider x = x as Element of T by A6;
A8: c2 . x = 0 by A2, A7, FUNCT_3:def_3;
A9: 0 c= 1 by XBOOLE_1:2;
reconsider a = c1 . x, b = c2 . x as Element of (BoolePoset 1) by A3;
 ex a, b being Element of S st
( a = c1 . x & b = c2 . x & a <= b ) by A5, YELLOW_2:def_1;
then A10: a <= b by A3, YELLOW_0:1;
 c1 . x = 1 by A1, A6, FUNCT_3:def_3;
then  1 c= 0 by A8, A10, YELLOW_1:2;
hence  contradiction by A9, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: YELLOW16:50
for L being non empty RelStr
for X being non empty set
for R being non empty full 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 ; ::_thesis: for X being non empty set
for R being non empty full 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
let X be non empty set ; ::_thesis: for R being non empty full 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
deffunc H1( set ) ->  Element of bool [:X,{$1}:] = X --> $1;
consider f being ManySortedSet of the carrier of L such that
A1: for i being Element of L holds f . i = H1(i) from PBOOLE:sch_5();
let R be non empty full SubRelStr of L |^ X; ::_thesis: ( ( for a being set holds
( a is Element of R iff ex x being Element of L st a = X --> x ) ) implies L,R are_isomorphic )
assume A2: for a being set holds
( a is Element of R iff ex x being Element of L st a = X --> x ) ; ::_thesis: L,R are_isomorphic
A3: rng f c= the carrier of R
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of R )
assume  y in rng f ; ::_thesis: y in the carrier of R
then consider x being set  such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def_3;
reconsider x = x as Element of L by A4;
 y = X --> x by A1, A5;
then  y is Element of R by A2;
hence  y in the carrier of R ; ::_thesis: verum
end;
A6: dom f = the carrier of L by PARTFUN1:def_2;
then reconsider f = f as Function of L,R by A3, FUNCT_2:2;
A7: f is V7()
proof
let x, y be Element of L; :: according to WAYBEL_1:def_1 ::_thesis: ( not f . x = f . y or x = y )
 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  ( not f . x = f . y or x = y ) by ZFMISC_1:3; ::_thesis: verum
end;
A9: now__::_thesis:_for_x,_y_being_Element_of_L_holds_
(_(_x_<=_y_implies_f_._x_<=_f_._y_)_&_(_f_._x_<=_f_._y_implies_x_<=_y_)_)
set i = the Element of X;
let x, y be Element of L; ::_thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
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)) ;
A10: (X --> L) . the Element of X = L by FUNCOP_1:7;
A11: f . y = X --> y by A1;
A12: f . x = X --> x by A1;
hereby  ::_thesis: ( f . x <= f . y implies x <= y )
assume A13: x <= y ; ::_thesis: f . x <= f . y
 Xx <= Xy
proof
let i be set ; :: according to YELLOW_2:def_1 ::_thesis: ( not i in X or ex b1, b2 being Element of the carrier of L st
( b1 = Xx . i & b2 = Xy . i & b1 <= b2 ) )
assume A14: i in X ; ::_thesis: ex b1, b2 being Element of the carrier of L st
( b1 = Xx . i & b2 = Xy . i & b1 <= b2 )
then A15: (X --> y) . i = y by FUNCOP_1:7;
 (X --> x) . i = x by A14, FUNCOP_1:7;
hence  ex b1, b2 being Element of the carrier of L st
( b1 = Xx . i & b2 = Xy . i & b1 <= b2 ) by A13, A15; ::_thesis: verum
end;
then  a <= b by A12, A11, WAYBEL10:11;
hence  f . x <= f . y by YELLOW_0:60; ::_thesis: verum
end;
assume  f . x <= f . y ; ::_thesis: x <= y
then  a <= b by YELLOW_0:59;
then  a9 . the Element of X <= b9 . the Element of X by WAYBEL_3:28;
then  x <= Xy . the Element of X by A12, A11, A10, FUNCOP_1:7;
hence  x <= y by FUNCOP_1:7; ::_thesis: verum
end;
take  f ; :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic
 rng f = the carrier of R
proof
thus  rng f c= the carrier of R ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of R c= rng f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in rng f )
assume  x in the carrier of R ; ::_thesis: x in rng f
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  x in rng f by A6, FUNCT_1:def_3; ::_thesis: verum
end;
hence  f is isomorphic by A7, A9, WAYBEL_0:66; ::_thesis: verum
end;

theorem :: YELLOW16:51
for S, T being non empty TopSpace holds
( S,T are_homeomorphic iff ex f being continuous Function of S,T ex g being continuous Function of T,S st
( f * g = id T & g * f = id S ) )
proof
let S, T be non empty TopSpace; ::_thesis: ( S,T are_homeomorphic iff ex f being continuous Function of S,T ex g being continuous Function of T,S st
( f * g = id T & g * f = id S ) )
hereby  ::_thesis: ( ex f being continuous Function of S,T ex g being continuous Function of T,S st
( f * g = id T & g * f = id S ) implies S,T are_homeomorphic )
assume  S,T are_homeomorphic ; ::_thesis: ex f being continuous Function of S,T ex g being continuous Function of T,S st
( f * g = id T & g * f = id S )
then consider f being Function of S,T such that
A1: f is being_homeomorphism by T_0TOPSP:def_1;
reconsider f = 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 = f; ::_thesis: ex g being continuous Function of T,S st
( f * g = id T & g * f = id S )
take g = g; ::_thesis: ( f * g = id T & g * f = id S )
A3: dom f = [#] S by A1, TOPS_2:def_5;
 f is V7() by A1, TOPS_2:def_5;
hence  ( f * g = id T & g * f = id S ) by A2, A3, TOPS_2:52; ::_thesis: verum
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 ; ::_thesis: S,T are_homeomorphic
A6: f is onto by A4, FUNCT_2:23;
then A7: rng f = [#] T by FUNCT_2:def_3;
take  f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism
A8: dom f = [#] S by FUNCT_2:def_1;
A9: f is V7() by A5, FUNCT_2:23;
then g = f " by A5, A7, FUNCT_2:30
.= f " by A6, A9, TOPS_2:def_4 ;
hence  f is being_homeomorphism by A9, A7, A8, TOPS_2:def_5; ::_thesis: verum
end;

theorem Th52: :: YELLOW16:52
for T, S, R being non empty TopSpace
for f being Function of T,S
for g being Function of S,T
for 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; ::_thesis: for f being Function of T,S
for g being Function of S,T
for h being Function of S,R st f * g = id S & h is being_homeomorphism holds
(h * f) * (g * (h ")) = id R
let f be Function of T,S; ::_thesis: for g being Function of S,T
for h being Function of S,R st f * g = id S & h is being_homeomorphism holds
(h * f) * (g * (h ")) = id R
let g be Function of S,T; ::_thesis: for h being Function of S,R st f * g = id S & h is being_homeomorphism holds
(h * f) * (g * (h ")) = id R
let h be Function of S,R; ::_thesis: ( f * g = id S & h is being_homeomorphism implies (h * f) * (g * (h ")) = id R )
assume that
A1: f * g = id S and
A2: h is being_homeomorphism ; ::_thesis: (h * f) * (g * (h ")) = id R
A3: h is V7() 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 ; ::_thesis: verum
end;

theorem Th53: :: YELLOW16:53
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; ::_thesis: ( S is_Retract_of T & S,R are_homeomorphic implies R is_Retract_of T )
given f being continuous Function of S,T, g being continuous Function of T,S such that A1: g * f = id S ; :: according to WAYBEL25:def_1 ::_thesis: ( not S,R are_homeomorphic or R is_Retract_of T )
given h being Function of S,R such that A2: h is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: R is_Retract_of T
 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 ; :: according to WAYBEL25:def_1 ::_thesis: ex b1 being Element of bool [: the carrier of T, the carrier of R:] st b1 * f9 = id R
take  g9 ; ::_thesis: g9 * f9 = id R
thus  g9 * f9 = id R by A1, A2, Th52; ::_thesis: verum
end;

theorem Th54: :: YELLOW16:54
for T being non empty TopSpace
for S being non empty SubSpace of T holds incl (S,T) is continuous
proof
let T be non empty TopSpace; ::_thesis: for S being non empty SubSpace of T holds incl (S,T) is continuous
let S be non empty SubSpace of T; ::_thesis: incl (S,T) is continuous
 incl (S,T) = id S by BORSUK_1:1, YELLOW_9:def_1;
hence  incl (S,T) is continuous by PRE_TOPC:26; ::_thesis: verum
end;

theorem Th55: :: YELLOW16:55
for T being non empty TopSpace
for S being non empty SubSpace of T
for 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; ::_thesis: for S being non empty SubSpace of T
for f being continuous Function of T,S st f is being_a_retraction holds
f * (incl (S,T)) = id S
let S be non empty SubSpace of T; ::_thesis: for f being continuous Function of T,S st f is being_a_retraction holds
f * (incl (S,T)) = id S
let f be continuous Function of T,S; ::_thesis: ( f is being_a_retraction implies f * (incl (S,T)) = id S )
assume A1: f is being_a_retraction ; ::_thesis: f * (incl (S,T)) = id S
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__::_thesis:_for_x_being_Element_of_S_holds_(f_*_(incl_(S,T)))_._x_=_(id_S)_._x
let x be Element of S; ::_thesis: (f * (incl (S,T))) . x = (id S) . x
 x in the carrier of S ;
then 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, FUNCT_1:18
.= y by A1, BORSUK_1:def_16
.= (id S) . x by FUNCT_1:18 ; ::_thesis: verum
end;
hence  f * (incl (S,T)) = id S by FUNCT_2:63; ::_thesis: verum
end;

theorem Th56: :: YELLOW16:56
for T being non empty TopSpace
for 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; ::_thesis: for S being non empty SubSpace of T st S is_a_retract_of T holds
S is_Retract_of T
let S be non empty SubSpace of T; ::_thesis: ( S is_a_retract_of T implies S is_Retract_of T )
reconsider g = incl (S,T) as continuous Function of S,T by Th54;
given f being continuous Function of T,S such that A1: f is being_a_retraction ; :: according to BORSUK_1:def_17 ::_thesis: S is_Retract_of T
take  g ; :: according to WAYBEL25:def_1 ::_thesis: ex b1 being Element of bool [: the carrier of T, the carrier of S:] st b1 * g = id S
take  f ; ::_thesis: f * g = id S
thus  f * g = id S by A1, Th55; ::_thesis: verum
end;

theorem :: YELLOW16:57
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; ::_thesis: ( 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 ) )
hereby  ::_thesis: ( ex S being non empty SubSpace of T st
( S is_a_retract_of T & S,R are_homeomorphic ) implies R is_Retract_of T )
assume  R is_Retract_of T ; ::_thesis: ex S being non empty SubSpace of T st
( S is_a_retract_of T & S,R are_homeomorphic )
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 = f as continuous Function of T,S by A1, WAYBEL18:10;
take S = S; ::_thesis: ( S is_a_retract_of T & S,R are_homeomorphic )
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__::_thesis:_for_x_being_Point_of_T_st_x_in_the_carrier_of_S_holds_
f_._x_=_x
let x be Point of T; ::_thesis: ( x in the carrier of S implies f . x = x )
assume  x in the carrier of S ; ::_thesis: f . x = x
then  x in [#] (T | rf) by WAYBEL18:def_6;
then  x in rng f by PRE_TOPC:def_5;
then  ex y being set st
( y in dom f & x = f . y ) by FUNCT_1:def_3;
hence  f . x = x by A2, FUNCT_1:13; ::_thesis: verum
end;
then  f is being_a_retraction by BORSUK_1:def_16;
hence  ( S is_a_retract_of T & S,R are_homeomorphic ) by A3, BORSUK_1:def_17; ::_thesis: verum
end;
given S being non empty SubSpace of T such that A5: S is_a_retract_of T and
A6: S,R are_homeomorphic ; ::_thesis: R is_Retract_of T
thus  R is_Retract_of T by A5, A6, Th53, Th56; ::_thesis: verum
end;