:: Retracts and Inheritance
:: by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


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 &amp; g9 = g &amp; f <= g holds
f9 <= g9
proofend;

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 &amp; g9 = g &amp; f9 <= g9 holds
f <= g
proofend;

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 &amp; b1 is monotone )
proofend;
end;

theorem :: YELLOW16:4
for f, g being Function st f is idempotent &amp; rng g c= rng f &amp; rng g c= dom f holds
f * g = g
proofend;

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
proofend;
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
proofend;

theorem Th6: :: YELLOW16:6
for L being non empty up-complete Poset
for f being Function of L,L st f is idempotent &amp; f is directed-sups-preserving holds
Image f is directed-sups-inheriting
proofend;

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
proofend;

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 &amp; f | the carrier of S = id S &amp; 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 &amp; 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 &amp; f | the carrier of S = id S &amp; 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 &amp; 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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 #)
proofend;

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 &amp; f is projection )
proofend;

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 &amp; ex g being monotone Function of T,S st
( f * g = id T &amp; g * f = id S ) ) )
proofend;

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 &amp; g * f = id S ) )
proofend;

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 &amp; T is_an_UPS_retract_of S )
proofend;

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 &amp; h | the carrier of (Image h) = id (Image h) &amp; S, Image h are_isomorphic )
proofend;

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 &amp; S, Image h are_isomorphic )
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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 &amp; b1 is reflexive-yielding )
proofend;
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
proofend;
end;

registration
let X be set ;
let S be Poset;
clusterX --> S ->  Poset-yielding ;
coherence
 X --> S is Poset-yielding
proofend;
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 &amp; b1 is non-Empty )
proofend;
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 &amp; product J is antisymmetric )
proofend;
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
proofend;
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))_)_&amp;_f_is_>=_than_X_&amp;_(_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)) ) &amp; f is_>=_than X &amp; ( 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)) ) &amp; f is_>=_than X &amp; ( 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)) ) &amp; f is_>=_than X &amp; ( 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)) ) &amp; f is_>=_than X &amp; ( 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)) ) &amp; f is_>=_than X &amp; ( 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 &amp; ( 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 toLATTICE3: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 toLATTICE3: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))_)_&amp;_f_is_<=_than_X_&amp;_(_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)) ) &amp; f is_<=_than X &amp; ( 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)) ) &amp; f is_<=_than X &amp; ( 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)) ) &amp; f is_<=_than X &amp; ( 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)) ) &amp; f is_<=_than X &amp; ( 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)) ) &amp; f is_<=_than X &amp; ( 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 &amp; ( 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 toLATTICE3: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 toLATTICE3: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) )
proofend;

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) )
proofend;

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 )
proofend;

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 )
proofend;

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))
proofend;

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))
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; sup X = "\/" (X,T) ) ) )
proofend;

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 &amp; inf X = "/\" (X,T) ) ) )
proofend;

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
proofend;

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()
proofend;

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
proofend;

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()
proofend;

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
proofend;
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
proofend;

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
proofend;
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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; not y in V holds
(chi (V, the carrier of T)) * ((0,1) --> (y,x)) = id Sierpinski_Space
proofend;

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) &amp; g = chi (W, the carrier of T) holds
( V c= W iff f <= g )
proofend;

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
proofend;

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 &amp; g * f = id S ) )
proofend;

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 &amp; h is being_homeomorphism holds
(h * f) * (g * (h ")) = id R
proofend;

theorem Th53: :: YELLOW16:53
for T, S, R being non empty TopSpace st S is_Retract_of T &amp; S,R are_homeomorphic holds
R is_Retract_of T
proofend;

theorem Th54: :: YELLOW16:54
for T being non empty TopSpace
for S being non empty SubSpace of T holds incl (S,T) is continuous
proofend;

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
proofend;

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
proofend;

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 &amp; S,R are_homeomorphic ) )
proofend;