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