yellow16.miz



    begin

    ::$Canceled

    theorem :: YELLOW16:2

    for X be set, L be non empty RelStr, S be non empty SubRelStr of L holds for f,g be Function of X, the carrier of S holds for f9,g9 be Function of X, the carrier of L st f9 = f & g9 = g & f <= g holds f9 <= g9

    proof

      let X be set, L be non empty RelStr, S be non empty SubRelStr of L;

      let f,g be Function of X, the carrier of S;

      let f9,g9 be Function of X, the carrier of L such that

       A1: f9 = f and

       A2: g9 = g and

       A3: f <= g;

      let x be set;

      assume

       A4: x in X;

      then

      reconsider a = (f . x), b = (g . x) as Element of S by FUNCT_2: 5;

      reconsider a9 = a, b9 = b as Element of L by YELLOW_0: 58;

      take a9, b9;

      thus a9 = (f9 . x) & b9 = (g9 . x) by A1, A2;

      ex a,b be Element of S st a = (f . x) & b = (g . x) & a <= b by A3, A4;

      hence thesis by YELLOW_0: 59;

    end;

    theorem :: YELLOW16:3

    for X be set, L be non empty RelStr holds for S be full non empty SubRelStr of L holds for f,g be Function of X, the carrier of S holds for f9,g9 be Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds f <= g

    proof

      let X be set, L be non empty RelStr;

      let S be full non empty SubRelStr of L;

      let f,g be Function of X, the carrier of S;

      let f9,g9 be Function of X, the carrier of L such that

       A1: f9 = f and

       A2: g9 = g and

       A3: f9 <= g9;

      let x be set;

      assume

       A4: x in X;

      then

      reconsider a = (f . x), b = (g . x) as Element of S by FUNCT_2: 5;

      take a, b;

      thus a = (f . x) & b = (g . x);

      ex a9,b9 be Element of L st a9 = a & b9 = b & a9 <= b9 by A1, A2, A3, A4;

      hence thesis by YELLOW_0: 60;

    end;

    registration

      let S be non empty RelStr;

      let T be non empty reflexive antisymmetric RelStr;

      cluster directed-sups-preserving monotone for Function of S, T;

      existence

      proof

        set x = the Element of T;

        take f = (S --> x);

        thus f is directed-sups-preserving

        proof

          let X be Subset of S;

          assume

           A1: X is non empty directed;

          

           A2: (f .: X) = {x}

          proof

            set a = the Element of X;

            thus (f .: X) c= {x} by FUNCOP_1: 81;

            

             A3: ( dom f) = the carrier of S;

            

             A4: a in X by A1;

            then (f . a) = x by FUNCOP_1: 7;

            then x in (f .: X) by A4, A3, FUNCT_1:def 6;

            hence thesis by ZFMISC_1: 31;

          end;

          assume ex_sup_of (X,S);

          thus ex_sup_of ((f .: X),T) by A2, YELLOW_0: 38;

          

          thus ( sup (f .: X)) = x by A2, YELLOW_0: 39

          .= (f . ( sup X));

        end;

        let a,b be Element of S;

        

         A5: x <= x;

        thus thesis by A5;

      end;

    end

    theorem :: YELLOW16:4

    for f,g be Function st f is idempotent & ( rng g) c= ( rng f) & ( rng g) c= ( dom f) holds (f * g) = g

    proof

      let f,g be Function;

      assume f is idempotent;

      then

       A1: (f * f) = f by QUANTAL1:def 9;

      assume

       A2: ( rng g) c= ( rng f);

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom g);

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

         A5: ex a be object st a in ( dom f) & (g . x) = (f . a) by A2, FUNCT_1:def 3;

        ((f * g) . x) = (f . (g . x)) by A4, FUNCT_1: 13;

        hence ((f * g) . x) = (g . x) by A1, A5, FUNCT_1: 13;

      end;

      assume ( rng g) c= ( dom f);

      then ( dom (f * g)) = ( dom g) by RELAT_1: 27;

      hence thesis by A3, FUNCT_1: 2;

    end;

    registration

      let S be 1-sorted;

      cluster idempotent for Function of S, S;

      existence

      proof

        take f = ( id S);

        (f * f) = f by FUNCT_2: 17;

        hence thesis by QUANTAL1:def 9;

      end;

    end

    theorem :: YELLOW16:5

    

     Th4: for L be up-complete non empty Poset holds for S be directed-sups-inheriting full non empty SubRelStr of L holds S is up-complete

    proof

      let L be up-complete non empty Poset;

      let S be directed-sups-inheriting full non empty SubRelStr of L;

      now

        let X be non empty directed Subset of S;

        reconsider Y = X as non empty directed Subset of L by YELLOW_2: 7;

         ex_sup_of (Y,L) by WAYBEL_0: 75;

        hence ex_sup_of (X,S) by WAYBEL_0: 7;

      end;

      hence thesis by WAYBEL_0: 75;

    end;

    theorem :: YELLOW16:6

    

     Th5: for L be up-complete non empty Poset holds for f be Function of L, L st f is idempotent directed-sups-preserving holds ( Image f) is directed-sups-inheriting

    proof

      let L be up-complete non empty Poset;

      let f be Function of L, L;

      set S = ( subrelstr ( rng f));

      set a = the Element of L;

      reconsider S9 = S as non empty full SubRelStr of L;

      assume

       A1: f is idempotent directed-sups-preserving;

      S is directed-sups-inheriting

      proof

        let X be directed Subset of S;

        X c= the carrier of S;

        then

         A2: X c= ( rng f) by YELLOW_0:def 15;

        assume X <> {} ;

        then X is non empty directed Subset of S9;

        then

        reconsider X9 = X as non empty directed Subset of L by YELLOW_2: 7;

        assume

         A3: ex_sup_of (X,L);

        f preserves_sup_of X9 by A1;

        then ( sup (f .: X9)) = (f . ( sup X9)) by A3;

        then ( sup X9) = (f . ( sup X9)) by A1, A2, YELLOW_2: 20;

        then ( "\/" (X,L)) in ( rng f) by FUNCT_2: 4;

        hence thesis by YELLOW_0:def 15;

      end;

      hence thesis;

    end;

    theorem :: YELLOW16:7

    

     Th6: for T be non empty RelStr, S be non empty SubRelStr of T holds for f be Function of T, S holds (f * ( incl (S,T))) = ( id S) implies f is idempotent Function of T, T

    proof

      let T be non empty RelStr, S be non empty SubRelStr of T;

      let f be Function of T, S;

      assume

       A1: (f * ( incl (S,T))) = ( id S);

      

       A2: the carrier of S c= the carrier of T by YELLOW_0:def 13;

      then ( incl (S,T)) = ( id the carrier of S) by YELLOW_9:def 1;

      then (( incl (S,T)) * f) = f by FUNCT_2: 17;

      

      then

       A3: (f * f) = (( id the carrier of S) * f) by A1, RELAT_1: 36

      .= f by FUNCT_2: 17;

      

       A4: ( dom f) = the carrier of T by FUNCT_2:def 1;

      f is onto by A1, FUNCT_2: 23;

      then ( rng f) = the carrier of S by FUNCT_2:def 3;

      hence thesis by A2, A3, A4, FUNCT_2: 2, QUANTAL1:def 9;

    end;

    definition

      let S,T be non empty Poset;

      let f be Function;

      :: YELLOW16:def1

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

      :: YELLOW16:def2

      pred f is_an_UPS_retraction_of T,S means f is directed-sups-preserving Function of T, S & ex g be directed-sups-preserving Function of S, T st (f * g) = ( id S);

    end

    definition

      let S,T be non empty Poset;

      :: YELLOW16:def3

      pred S is_a_retract_of T means ex f be Function of T, S st f is_a_retraction_of (T,S);

      :: YELLOW16:def4

      pred S is_an_UPS_retract_of T means ex f be Function of T, S st f is_an_UPS_retraction_of (T,S);

    end

    theorem :: YELLOW16:8

    

     Th7: for S,T be non empty Poset, f be Function st f is_a_retraction_of (T,S) holds (f * ( incl (S,T))) = ( id S)

    proof

      let S,T be non empty Poset, f be Function such that f is directed-sups-preserving Function of T, S and

       A1: (f | the carrier of S) = ( id S) and

       A2: S is directed-sups-inheriting full SubRelStr of T;

      the carrier of S c= the carrier of T by A2, YELLOW_0:def 13;

      

      hence (f * ( incl (S,T))) = (f * ( id the carrier of S)) by YELLOW_9:def 1

      .= ( id S) by A1, RELAT_1: 65;

    end;

    theorem :: YELLOW16:9

    

     Th8: for S be non empty Poset, T be up-complete non empty Poset holds for f be Function st f is_a_retraction_of (T,S) holds f is_an_UPS_retraction_of (T,S)

    proof

      let S be non empty Poset;

      let T be up-complete non empty Poset, f be Function;

      assume

       A1: f is_a_retraction_of (T,S);

      hence f is directed-sups-preserving Function of T, S;

      S is directed-sups-inheriting full SubRelStr of T by A1;

      then

      reconsider g = ( incl (S,T)) as directed-sups-preserving Function of S, T by WAYBEL21: 10;

      take g;

      thus thesis by A1, Th7;

    end;

    theorem :: YELLOW16:10

    

     Th9: for S,T be non empty Poset, f be Function st f is_a_retraction_of (T,S) holds ( rng f) = the carrier of S

    proof

      let S,T be non empty Poset, f be Function;

      assume

       A1: f is_a_retraction_of (T,S);

      then

      reconsider f as Function of T, S;

      (f * ( incl (S,T))) = ( id S) by A1, Th7;

      then f is onto by FUNCT_2: 23;

      hence thesis by FUNCT_2:def 3;

    end;

    theorem :: YELLOW16:11

    

     Th10: for S,T be non empty Poset, f be Function st f is_an_UPS_retraction_of (T,S) holds ( rng f) = the carrier of S

    proof

      let S,T be non empty Poset, f be Function;

      assume that

       A1: f is directed-sups-preserving Function of T, S and

       A2: ex g be directed-sups-preserving Function of S, T st (f * g) = ( id S);

      reconsider f as Function of T, S by A1;

      f is onto by A2, FUNCT_2: 23;

      hence thesis by FUNCT_2:def 3;

    end;

    theorem :: YELLOW16:12

    

     Th11: for S,T be non empty Poset, f be Function st f is_a_retraction_of (T,S) holds f is idempotent Function of T, T

    proof

      let S,T be non empty Poset, f be Function;

      assume

       A1: f is_a_retraction_of (T,S);

      then

       A2: f is Function of T, S;

      

       A3: S is SubRelStr of T by A1;

      (f * ( incl (S,T))) = ( id S) by A1, Th7;

      hence thesis by A2, A3, Th6;

    end;

    theorem :: YELLOW16:13

    

     Th12: for T,S be non empty Poset, f be Function of T, T st f is_a_retraction_of (T,S) holds ( Image f) = the RelStr of S

    proof

      let T,S be non empty Poset, f be Function of T, T;

      

       A1: the carrier of ( Image f) = ( rng f) by YELLOW_0:def 15;

      assume

       A2: f is_a_retraction_of (T,S);

      thus thesis by A2, A1, Th9, YELLOW_0: 57;

    end;

    theorem :: YELLOW16:14

    

     Th13: for T be up-complete non empty Poset holds for S be non empty Poset, f be Function of T, T st f is_a_retraction_of (T,S) holds f is directed-sups-preserving projection

    proof

      let T be up-complete non empty Poset;

      let S be non empty Poset, f be Function of T, T;

      assume

       A1: f is_a_retraction_of (T,S);

      then

      reconsider g = f as directed-sups-preserving Function of T, S;

      f is idempotent by A1, Th11;

      

      then

       A2: f = (f * f) by QUANTAL1:def 9

      .= ((f | ( rng f)) * f) by FUNCT_4: 2

      .= ((f | the carrier of S) * f) by A1, Th8, Th10

      .= (( id S) * f) by A1

      .= (( id the carrier of S) * g);

      

       A3: S is full directed-sups-inheriting non empty SubRelStr of T by A1;

      then

       A4: ( incl (S,T)) is directed-sups-preserving by WAYBEL21: 10;

      the carrier of S c= the carrier of T by A3, YELLOW_0:def 13;

      then

       A5: ( incl (S,T)) = ( id the carrier of S) by YELLOW_9:def 1;

      hence f is directed-sups-preserving by A2, A4, WAYBEL20: 28;

      f is directed-sups-preserving idempotent Function of T, T by A1, A2, A4, A5, Th11, WAYBEL20: 28;

      hence thesis;

    end;

    theorem :: YELLOW16:15

    

     Th14: for S,T be non empty reflexive transitive RelStr holds for f be Function of S, T holds f is isomorphic iff f is monotone & ex g be monotone Function of T, S st (f * g) = ( id T) & (g * f) = ( id S)

    proof

      let S,T be non empty reflexive transitive RelStr, f be Function of S, T;

      hereby

        assume

         A1: f is isomorphic;

        hence f is monotone;

        consider g be Function of T, S such that

         A2: g = (f qua Function " ) and

         A3: g is monotone by A1, WAYBEL_0:def 38;

        reconsider g as monotone Function of T, S by A3;

        take g;

        ( rng f) = the carrier of T by A1, WAYBEL_0: 66;

        hence (f * g) = ( id T) & (g * f) = ( id S) by A1, A2, FUNCT_2: 29;

      end;

      assume

       A4: f is monotone;

      given g be monotone Function of T, S such that

       A5: (f * g) = ( id T) and

       A6: (g * f) = ( id S);

      

       A7: f is one-to-one by A6, FUNCT_2: 23;

      f is onto by A5, FUNCT_2: 23;

      then ( rng f) = the carrier of T by FUNCT_2:def 3;

      then g = (f qua Function " ) by A6, A7, FUNCT_2: 30;

      hence thesis by A4, A7, WAYBEL_0:def 38;

    end;

    theorem :: YELLOW16:16

    

     Th15: for S,T be non empty Poset holds (S,T) are_isomorphic iff ex f be monotone Function of S, T, g be monotone Function of T, S st (f * g) = ( id T) & (g * f) = ( id S)

    proof

      let S,T be non empty Poset;

      hereby

        assume (S,T) are_isomorphic ;

        then

        consider f be Function of S, T such that

         A1: f is isomorphic;

        reconsider f as monotone Function of S, T by A1;

        consider g be Function of T, S such that

         A2: g = (f qua Function " ) and

         A3: g is monotone by A1, WAYBEL_0:def 38;

        take f;

        reconsider g as monotone Function of T, S by A3;

        take g;

        ( rng f) = the carrier of T by A1, WAYBEL_0: 66;

        hence (f * g) = ( id T) & (g * f) = ( id S) by A1, A2, FUNCT_2: 29;

      end;

      given f be monotone Function of S, T, g be monotone Function of T, S such that

       A4: (f * g) = ( id T) and

       A5: (g * f) = ( id S);

      take f;

      

       A6: f is one-to-one by A5, FUNCT_2: 23;

      f is onto by A4, FUNCT_2: 23;

      then ( rng f) = the carrier of T by FUNCT_2:def 3;

      then g = (f qua Function " ) by A5, A6, FUNCT_2: 30;

      hence thesis by A6, WAYBEL_0:def 38;

    end;

    theorem :: YELLOW16:17

    for S,T be up-complete non empty Poset st (S,T) are_isomorphic holds S is_an_UPS_retract_of T & T is_an_UPS_retract_of S

    proof

      let S,T be up-complete non empty Poset;

      assume (S,T) are_isomorphic ;

      then

      consider f be monotone Function of S, T, g be monotone Function of T, S such that

       A1: (f * g) = ( id T) and

       A2: (g * f) = ( id S) by Th15;

      g is isomorphic by A1, A2, Th14;

      then

       A3: g is sups-preserving by WAYBEL13: 20;

      f is isomorphic by A1, A2, Th14;

      then

       A4: f is sups-preserving by WAYBEL13: 20;

      then

       A5: f is_an_UPS_retraction_of (S,T) by A1, A3;

      g is_an_UPS_retraction_of (T,S) by A2, A4, A3;

      hence thesis by A5;

    end;

    theorem :: YELLOW16:18

    

     Th17: for T,S be non empty Poset holds for f be monotone Function of T, S, g be monotone Function of S, T st (f * g) = ( id S) holds ex h be projection Function of T, T st h = (g * f) & (h | the carrier of ( Image h)) = ( id ( Image h)) & (S,( Image h)) are_isomorphic

    proof

      let T,S be non empty Poset;

      let f be monotone Function of T, S, g be monotone Function of S, T such that

       A1: (f * g) = ( id S);

      set h = (g * f);

      (h * h) = ((h * g) * f) by RELAT_1: 36

      .= ((g * ( id S)) * f) by A1, RELAT_1: 36

      .= h by FUNCT_2: 17;

      then h is idempotent monotone Function of T, T by QUANTAL1:def 9, YELLOW_2: 12;

      then

      reconsider h as projection Function of T, T by WAYBEL_1:def 13;

      

       A2: ( dom g) = the carrier of S by FUNCT_2:def 1;

      f is onto by A1, FUNCT_2: 23;

      then

       A3: ( rng f) = the carrier of S by FUNCT_2:def 3;

      then

      reconsider gg = ( corestr g) as Function of S, ( Image h) by A2, RELAT_1: 28;

      

       A4: gg = g by WAYBEL_1: 30;

       A5:

      now

        let x,y be Element of S;

        x <= y implies (g . x) <= (g . y) & (gg . x) in the carrier of ( Image h) by WAYBEL_1:def 2;

        hence x <= y implies (gg . x) <= (gg . y) by A4, YELLOW_0: 60;

        (( id S) . x) = x;

        then

         A6: x = (f . (g . x)) by A1, FUNCT_2: 15;

        (( id S) . y) = y;

        then

         A7: y = (f . (g . y)) by A1, FUNCT_2: 15;

        assume (gg . x) <= (gg . y);

        then (g . x) <= (g . y) by A4, YELLOW_0: 59;

        hence x <= y by A6, A7, WAYBEL_1:def 2;

      end;

      ( rng h) = ( rng g) by A3, A2, RELAT_1: 28;

      then

       A8: ( rng gg) = the carrier of ( Image h) by A4, YELLOW_0:def 15;

      take h;

      thus h = (g * f);

      

      thus (h | the carrier of ( Image h)) = (h * ( inclusion h)) by RELAT_1: 65

      .= (( corestr h) * ( inclusion h)) by WAYBEL_1: 30

      .= ( id ( Image h)) by WAYBEL_1: 33;

      take gg;

      gg is one-to-one by A1, A4, FUNCT_2: 23;

      hence thesis by A8, A5, WAYBEL_0: 66;

    end;

    theorem :: YELLOW16:19

    

     Th18: for T be up-complete non empty Poset, S be non empty Poset holds for f be Function st f is_an_UPS_retraction_of (T,S) holds ex h be directed-sups-preserving projection Function of T, T st h is_a_retraction_of (T,( Image h)) & (S,( Image h)) are_isomorphic

    proof

      let T be up-complete non empty Poset;

      let S be non empty Poset, f be Function such that

       A1: f is directed-sups-preserving Function of T, S;

      given g be directed-sups-preserving Function of S, T such that

       A2: (f * g) = ( id S);

      reconsider f as directed-sups-preserving Function of T, S by A1;

      consider h be projection Function of T, T such that

       A3: h = (g * f) and

       A4: (h | the carrier of ( Image h)) = ( id ( Image h)) and

       A5: (S,( Image h)) are_isomorphic by A2, Th17;

      reconsider h as directed-sups-preserving projection Function of T, T by A3, WAYBEL20: 28;

      take h;

      reconsider R = ( Image h) as non empty Poset;

      h = ( corestr h) by WAYBEL_1: 30;

      then

       A6: h is directed-sups-preserving Function of T, R by WAYBEL20: 22;

      R is directed-sups-inheriting full SubRelStr of T by Th5;

      hence h is_a_retraction_of (T,( Image h)) by A4, A6;

      thus thesis by A5;

    end;

    theorem :: YELLOW16:20

    

     Th19: for L be up-complete non empty Poset holds for S be non empty Poset st S is_a_retract_of L holds S is up-complete

    proof

      let L be up-complete non empty Poset;

      let S be non empty Poset;

      given f be Function of L, S such that

       A1: f is_a_retraction_of (L,S);

      S is full directed-sups-inheriting non empty SubRelStr of L by A1;

      hence thesis by Th4;

    end;

    theorem :: YELLOW16:21

    

     Th20: for L be complete non empty Poset holds for S be non empty Poset st S is_a_retract_of L holds S is complete

    proof

      let L be complete non empty Poset;

      let S be non empty Poset;

      given f be Function of L, S such that

       A1: f is_a_retraction_of (L,S);

      reconsider f as directed-sups-preserving projection Function of L, L by A1, Th11, Th13;

      

       A2: ( Image f) is complete by YELLOW_2: 35;

       the RelStr of S = ( Image f) by A1, Th12;

      hence thesis by A2, YELLOW_0: 3;

    end;

    theorem :: YELLOW16:22

    

     Th21: for L be continuous complete LATTICE holds for S be non empty Poset st S is_a_retract_of L holds S is continuous

    proof

      let L be continuous complete LATTICE;

      let S be non empty Poset;

      given f be Function of L, S such that

       A1: f is_a_retraction_of (L,S);

      reconsider g = f as directed-sups-preserving projection Function of L, L by A1, Th11, Th13;

      

       A2: ( Image g) is continuous LATTICE by WAYBEL15: 15;

      ( Image g) = the RelStr of S by A1, Th12;

      hence thesis by A2, YELLOW12: 15;

    end;

    theorem :: YELLOW16:23

    for L be up-complete non empty Poset holds for S be non empty Poset st S is_an_UPS_retract_of L holds S is up-complete

    proof

      let L be up-complete non empty Poset;

      let S be non empty Poset;

      given f be Function of L, S such that

       A1: f is_an_UPS_retraction_of (L,S);

      consider h be directed-sups-preserving projection Function of L, L such that

       A2: h is_a_retraction_of (L,( Image h)) and

       A3: (S,( Image h)) are_isomorphic by A1, Th18;

      ( Image h) is_a_retract_of L by A2;

      then ( Image h) is up-complete by Th19;

      hence thesis by A3, WAYBEL13: 30, WAYBEL_1: 6;

    end;

    theorem :: YELLOW16:24

    for L be complete non empty Poset holds for S be non empty Poset st S is_an_UPS_retract_of L holds S is complete

    proof

      let L be complete non empty Poset, S be non empty Poset;

      given f be Function of L, S such that

       A1: f is_an_UPS_retraction_of (L,S);

      consider h be directed-sups-preserving projection Function of L, L such that

       A2: h is_a_retraction_of (L,( Image h)) and

       A3: (S,( Image h)) are_isomorphic by A1, Th18;

      ( Image h) is_a_retract_of L by A2;

      then ( Image h) is complete by Th20;

      hence thesis by A3, WAYBEL20: 18, WAYBEL_1: 6;

    end;

    theorem :: YELLOW16:25

    for L be continuous complete LATTICE holds for S be non empty Poset st S is_an_UPS_retract_of L holds S is continuous

    proof

      let L be continuous complete LATTICE;

      let S be non empty Poset;

      given f be Function of L, S such that

       A1: f is_an_UPS_retraction_of (L,S);

      consider h be directed-sups-preserving projection Function of L, L such that

       A2: h is_a_retraction_of (L,( Image h)) and

       A3: (S,( Image h)) are_isomorphic by A1, Th18;

      ( Image h) is_a_retract_of L by A2;

      then ( Image h) is continuous by Th21;

      hence thesis by A3, WAYBEL15: 9, WAYBEL_1: 6;

    end;

    theorem :: YELLOW16:26

    

     Th25: for L be RelStr holds for S be full SubRelStr of L holds for R be SubRelStr of S holds R is full iff R is full SubRelStr of L

    proof

      let L be RelStr, S be full SubRelStr of L, R be SubRelStr of S;

      reconsider R9 = R as SubRelStr of L by YELLOW_6: 7;

      

       A1: the carrier of R c= the carrier of S by YELLOW_0:def 13;

      hereby

        assume R is full;

        

        then the InternalRel of R = (the InternalRel of S |_2 the carrier of R)

        .= ((the InternalRel of L |_2 the carrier of S) |_2 the carrier of R) by YELLOW_0:def 14

        .= (the InternalRel of L |_2 the carrier of R9) by A1, WELLORD1: 22;

        hence R is full SubRelStr of L by YELLOW_0:def 14;

      end;

      assume

       A2: R is full SubRelStr of L;

      ((the InternalRel of L |_2 the carrier of S) |_2 the carrier of R) = (the InternalRel of L |_2 the carrier of R) by A1, WELLORD1: 22

      .= the InternalRel of R by A2, YELLOW_0:def 14;

      hence the InternalRel of R = (the InternalRel of S |_2 the carrier of R) by YELLOW_0:def 14;

    end;

    theorem :: YELLOW16:27

    for L be non empty transitive RelStr holds for S be directed-sups-inheriting non empty full SubRelStr of L holds for R be directed-sups-inheriting non empty SubRelStr of S holds R is directed-sups-inheriting SubRelStr of L

    proof

      let L be non empty transitive RelStr;

      let S be directed-sups-inheriting non empty full SubRelStr of L;

      let R be directed-sups-inheriting non empty SubRelStr of S;

      reconsider T = R as SubRelStr of L by YELLOW_6: 7;

      T is directed-sups-inheriting

      proof

        let X be directed Subset of T;

        reconsider Y = X as directed Subset of S by YELLOW_2: 7;

        assume

         A1: X <> {} ;

        assume

         A2: ex_sup_of (X,L);

        then

         A3: ex_sup_of (Y,S) by A1, WAYBEL_0: 7;

        ( sup Y) = ( "\/" (X,L)) by A1, A2, WAYBEL_0: 7;

        hence thesis by A1, A3, WAYBEL_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: YELLOW16:28

    for L be up-complete non empty Poset holds for S1,S2 be directed-sups-inheriting full non empty SubRelStr of L st S1 is SubRelStr of S2 holds S1 is directed-sups-inheriting full SubRelStr of S2

    proof

      let L be up-complete non empty Poset;

      let S1,S2 be directed-sups-inheriting full non empty SubRelStr of L;

      assume S1 is SubRelStr of S2;

      then

      reconsider S = S1 as SubRelStr of S2;

      S is directed-sups-inheriting

      proof

        let X be directed Subset of S;

        assume X <> {} ;

        then

        reconsider Y1 = X as non empty directed Subset of S1;

        reconsider Y2 = Y1 as non empty directed Subset of S2 by YELLOW_2: 7;

        reconsider Y = Y1 as non empty directed Subset of L by YELLOW_2: 7;

        

         A1: ex_sup_of (Y,L) by WAYBEL_0: 75;

        then

         A2: ( sup Y) = ( sup Y1) by WAYBEL_0: 7;

        ( sup Y2) = ( sup Y) by A1, WAYBEL_0: 7;

        hence thesis by A2;

      end;

      hence thesis by Th25;

    end;

    begin

    definition

      let R be Relation;

      :: YELLOW16:def5

      attr R is Poset-yielding means

      : Def5: for x be set st x in ( rng R) holds x is Poset;

    end

    registration

      cluster Poset-yielding -> RelStr-yielding reflexive-yielding for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A1: for x be set st x in ( rng R) holds x is Poset;

        hence for x be set st x in ( rng R) holds x is RelStr;

        thus for S be RelStr st S in ( rng R) holds S is reflexive by A1;

      end;

    end

    definition

      let X be non empty set;

      let L be non empty RelStr;

      let i be Element of X;

      let Y be Subset of (L |^ X);

      :: original: pi

      redefine

      func pi (Y,i) -> Subset of L ;

      coherence

      proof

        reconsider Y9 = Y as Subset of ( product (X --> L));

        ( pi (Y9,i)) is Subset of ((X --> L) . i);

        hence thesis;

      end;

    end

    registration

      let X be set;

      let S be Poset;

      cluster (X --> S) -> Poset-yielding;

      coherence

      proof

        let x be set;

        assume x in ( rng (X --> S));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let I be set;

      cluster Poset-yielding non-Empty for ManySortedSet of I;

      existence

      proof

        set P = the non empty Poset;

        take (I --> P);

        thus thesis;

      end;

    end

    registration

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      cluster ( product J) -> transitive antisymmetric;

      coherence

      proof

         A1:

        now

          let i be Element of I;

          ( dom J) = I by PARTFUN1:def 2;

          then (J . i) in ( rng J) by FUNCT_1:def 3;

          hence (J . i) is Poset by Def5;

        end;

        then for i be Element of I holds (J . i) is transitive;

        hence ( product J) is transitive by WAYBEL_3: 29;

        for i be Element of I holds (J . i) is antisymmetric by A1;

        hence thesis by WAYBEL_3: 30;

      end;

    end

    definition

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let i be Element of I;

      :: original: .

      redefine

      func J . i -> non empty Poset ;

      coherence

      proof

        ( dom J) = I by PARTFUN1:def 2;

        then (J . i) in ( rng J) by FUNCT_1:def 3;

        hence thesis by Def5;

      end;

    end

     Lm1:

    now

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let X be Subset of ( product J);

      deffunc F( Element of I) = ( sup ( pi (X,$1)));

      consider f be ManySortedSet of I such that

       A1: for i be Element of I holds (f . i) = F(i) from PBOOLE:sch 5;

       A2:

      now

        let i be Element of I;

        (f . i) = ( sup ( pi (X,i))) by A1;

        hence (f . i) is Element of (J . i);

      end;

      ( dom f) = I by PARTFUN1:def 2;

      then

      reconsider f as Element of ( product J) by A2, WAYBEL_3: 27;

      assume

       A3: for i be Element of I holds ex_sup_of (( pi (X,i)),(J . i));

      take f;

      thus for i be Element of I holds (f . i) = ( sup ( pi (X,i))) by A1;

      thus f is_>=_than X

      proof

        let x be Element of ( product J) such that

         A4: x in X;

        now

          let i be Element of I;

          

           A5: (f . i) = ( sup ( pi (X,i))) by A1;

          

           A6: (x . i) in ( pi (X,i)) by A4, CARD_3:def 6;

           ex_sup_of (( pi (X,i)),(J . i)) by A3;

          then (f . i) is_>=_than ( pi (X,i)) by A5, YELLOW_0: 30;

          hence (x . i) <= (f . i) by A6;

        end;

        hence thesis by WAYBEL_3: 28;

      end;

      let g be Element of ( product J);

      assume

       A7: X is_<=_than g;

      now

        let i be Element of I;

        

         A8: ex_sup_of (( pi (X,i)),(J . i)) by A3;

        

         A9: (g . i) is_>=_than ( pi (X,i))

        proof

          let a be Element of (J . i);

          assume a in ( pi (X,i));

          then

          consider h be Function such that

           A10: h in X and

           A11: a = (h . i) by CARD_3:def 6;

          reconsider h as Element of ( product J) by A10;

          h <= g by A7, A10;

          hence a <= (g . i) by A11, WAYBEL_3: 28;

        end;

        (f . i) = ( sup ( pi (X,i))) by A1;

        hence (f . i) <= (g . i) by A8, A9, YELLOW_0: 30;

      end;

      hence f <= g by WAYBEL_3: 28;

    end;

     Lm2:

    now

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let X be Subset of ( product J);

      deffunc F( Element of I) = ( inf ( pi (X,$1)));

      consider f be ManySortedSet of I such that

       A1: for i be Element of I holds (f . i) = F(i) from PBOOLE:sch 5;

       A2:

      now

        let i be Element of I;

        (f . i) = ( inf ( pi (X,i))) by A1;

        hence (f . i) is Element of (J . i);

      end;

      ( dom f) = I by PARTFUN1:def 2;

      then

      reconsider f as Element of ( product J) by A2, WAYBEL_3: 27;

      assume

       A3: for i be Element of I holds ex_inf_of (( pi (X,i)),(J . i));

      take f;

      thus for i be Element of I holds (f . i) = ( inf ( pi (X,i))) by A1;

      thus f is_<=_than X

      proof

        let x be Element of ( product J) such that

         A4: x in X;

        now

          let i be Element of I;

          

           A5: (f . i) = ( inf ( pi (X,i))) by A1;

          

           A6: (x . i) in ( pi (X,i)) by A4, CARD_3:def 6;

           ex_inf_of (( pi (X,i)),(J . i)) by A3;

          then (f . i) is_<=_than ( pi (X,i)) by A5, YELLOW_0: 31;

          hence (x . i) >= (f . i) by A6;

        end;

        hence thesis by WAYBEL_3: 28;

      end;

      let g be Element of ( product J);

      assume

       A7: X is_>=_than g;

      now

        let i be Element of I;

        

         A8: ex_inf_of (( pi (X,i)),(J . i)) by A3;

        

         A9: (g . i) is_<=_than ( pi (X,i))

        proof

          let a be Element of (J . i);

          assume a in ( pi (X,i));

          then

          consider h be Function such that

           A10: h in X and

           A11: a = (h . i) by CARD_3:def 6;

          reconsider h as Element of ( product J) by A10;

          h >= g by A7, A10;

          hence a >= (g . i) by A11, WAYBEL_3: 28;

        end;

        (f . i) = ( inf ( pi (X,i))) by A1;

        hence (f . i) >= (g . i) by A8, A9, YELLOW_0: 31;

      end;

      hence f >= g by WAYBEL_3: 28;

    end;

    theorem :: YELLOW16:29

    

     Th28: for I be non empty set holds for J be Poset-yielding non-Empty ManySortedSet of I holds for f be Element of ( product J), X be Subset of ( product J) holds f is_>=_than X iff for i be Element of I holds (f . i) is_>=_than ( pi (X,i))

    proof

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let f be Element of ( product J), X be Subset of ( product J);

      hereby

        assume

         A1: f is_>=_than X;

        let i be Element of I;

        thus (f . i) is_>=_than ( pi (X,i))

        proof

          let x be Element of (J . i);

          assume x in ( pi (X,i));

          then

          consider g be Function such that

           A2: g in X and

           A3: x = (g . i) by CARD_3:def 6;

          reconsider g as Element of ( product J) by A2;

          g <= f by A1, A2;

          hence thesis by A3, WAYBEL_3: 28;

        end;

      end;

      assume

       A4: for i be Element of I holds (f . i) is_>=_than ( pi (X,i));

      let g be Element of ( product J);

      assume

       A5: g in X;

      now

        let i be Element of I;

        

         A6: (f . i) is_>=_than ( pi (X,i)) by A4;

        (g . i) in ( pi (X,i)) by A5, CARD_3:def 6;

        hence (g . i) <= (f . i) by A6;

      end;

      hence thesis by WAYBEL_3: 28;

    end;

    theorem :: YELLOW16:30

    

     Th29: for I be non empty set holds for J be Poset-yielding non-Empty ManySortedSet of I holds for f be Element of ( product J), X be Subset of ( product J) holds f is_<=_than X iff for i be Element of I holds (f . i) is_<=_than ( pi (X,i))

    proof

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let f be Element of ( product J), X be Subset of ( product J);

      hereby

        assume

         A1: f is_<=_than X;

        let i be Element of I;

        thus (f . i) is_<=_than ( pi (X,i))

        proof

          let x be Element of (J . i);

          assume x in ( pi (X,i));

          then

          consider g be Function such that

           A2: g in X and

           A3: x = (g . i) by CARD_3:def 6;

          reconsider g as Element of ( product J) by A2;

          g >= f by A1, A2;

          hence thesis by A3, WAYBEL_3: 28;

        end;

      end;

      assume

       A4: for i be Element of I holds (f . i) is_<=_than ( pi (X,i));

      let g be Element of ( product J);

      assume

       A5: g in X;

      now

        let i be Element of I;

        

         A6: (f . i) is_<=_than ( pi (X,i)) by A4;

        (g . i) in ( pi (X,i)) by A5, CARD_3:def 6;

        hence (g . i) >= (f . i) by A6;

      end;

      hence thesis by WAYBEL_3: 28;

    end;

    theorem :: YELLOW16:31

    

     Th30: for I be non empty set holds for J be Poset-yielding non-Empty ManySortedSet of I holds for X be Subset of ( product J) holds ex_sup_of (X,( product J)) iff for i be Element of I holds ex_sup_of (( pi (X,i)),(J . i))

    proof

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let X be Subset of ( product J);

      hereby

        set f = ( sup X);

        assume

         A1: ex_sup_of (X,( product J));

        let i be Element of I;

         A2:

        now

          let x be Element of (J . i);

          assume

           A3: ( pi (X,i)) is_<=_than x;

          set g = (f +* (i,x));

          

           A4: ( dom g) = ( dom f) by FUNCT_7: 30;

          ( dom f) = I by WAYBEL_3: 27;

          then

           A5: (g . i) = x by FUNCT_7: 31;

          now

            let j be Element of I;

            (g . j) = (f . j) or (g . j) = x & j = i by A5, FUNCT_7: 32;

            hence (g . j) is Element of (J . j);

          end;

          then

          reconsider g as Element of ( product J) by A4, WAYBEL_3: 27;

          

           A6: X is_<=_than f by A1, YELLOW_0: 30;

          X is_<=_than g

          proof

            let h be Element of ( product J);

            assume

             A7: h in X;

            then

             A8: (h . i) in ( pi (X,i)) by CARD_3:def 6;

            

             A9: h <= f by A6, A7;

            now

              let j be Element of I;

              (g . j) = (f . j) or (g . j) = x & j = i by A5, FUNCT_7: 32;

              hence (h . j) <= (g . j) by A3, A9, A8, WAYBEL_3: 28;

            end;

            hence h <= g by WAYBEL_3: 28;

          end;

          then f <= g by A1, YELLOW_0: 30;

          hence (f . i) <= x by A5, WAYBEL_3: 28;

        end;

        f is_>=_than X by A1, YELLOW_0: 30;

        then (f . i) is_>=_than ( pi (X,i)) by Th28;

        hence ex_sup_of (( pi (X,i)),(J . i)) by A2, YELLOW_0: 30;

      end;

      assume for i be Element of I holds ex_sup_of (( pi (X,i)),(J . i));

      then ex f be Element of ( product J) st (for i be Element of I holds (f . i) = ( sup ( pi (X,i)))) & f is_>=_than X & for g be Element of ( product J) st X is_<=_than g holds f <= g by Lm1;

      hence thesis by YELLOW_0: 30;

    end;

    theorem :: YELLOW16:32

    

     Th31: for I be non empty set holds for J be Poset-yielding non-Empty ManySortedSet of I holds for X be Subset of ( product J) holds ex_inf_of (X,( product J)) iff for i be Element of I holds ex_inf_of (( pi (X,i)),(J . i))

    proof

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let X be Subset of ( product J);

      hereby

        set f = ( inf X);

        assume

         A1: ex_inf_of (X,( product J));

        let i be Element of I;

        

         A2: f is_<=_than X by A1, YELLOW_0: 31;

         A3:

        now

          let x be Element of (J . i);

          set g = (f +* (i,x));

          

           A4: ( dom g) = ( dom f) by FUNCT_7: 30;

          ( dom f) = I by WAYBEL_3: 27;

          then

           A5: (g . i) = x by FUNCT_7: 31;

          now

            let j be Element of I;

            (g . j) = (f . j) or (g . j) = x & j = i by A5, FUNCT_7: 32;

            hence (g . j) is Element of (J . j);

          end;

          then

          reconsider g as Element of ( product J) by A4, WAYBEL_3: 27;

          assume

           A6: ( pi (X,i)) is_>=_than x;

          X is_>=_than g

          proof

            let h be Element of ( product J);

            assume

             A7: h in X;

            then

             A8: (h . i) in ( pi (X,i)) by CARD_3:def 6;

            

             A9: h >= f by A2, A7;

            now

              let j be Element of I;

              (g . j) = (f . j) or (g . j) = x & j = i by A5, FUNCT_7: 32;

              hence (h . j) >= (g . j) by A6, A9, A8, WAYBEL_3: 28;

            end;

            hence thesis by WAYBEL_3: 28;

          end;

          then f >= g by A1, YELLOW_0: 31;

          hence (f . i) >= x by A5, WAYBEL_3: 28;

        end;

        (f . i) is_<=_than ( pi (X,i)) by A2, Th29;

        hence ex_inf_of (( pi (X,i)),(J . i)) by A3, YELLOW_0: 31;

      end;

      assume for i be Element of I holds ex_inf_of (( pi (X,i)),(J . i));

      then ex f be Element of ( product J) st (for i be Element of I holds (f . i) = ( inf ( pi (X,i)))) & f is_<=_than X & for g be Element of ( product J) st X is_>=_than g holds f >= g by Lm2;

      hence thesis by YELLOW_0: 31;

    end;

    theorem :: YELLOW16:33

    

     Th32: for I be non empty set holds for J be Poset-yielding non-Empty ManySortedSet of I holds for X be Subset of ( product J) st ex_sup_of (X,( product J)) holds for i be Element of I holds (( sup X) . i) = ( sup ( pi (X,i)))

    proof

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let X be Subset of ( product J);

      assume ex_sup_of (X,( product J));

      then for i be Element of I holds ex_sup_of (( pi (X,i)),(J . i)) by Th30;

      then

      consider f be Element of ( product J) such that

       A1: for i be Element of I holds (f . i) = ( sup ( pi (X,i))) and

       A2: f is_>=_than X and

       A3: for g be Element of ( product J) st X is_<=_than g holds f <= g by Lm1;

      ( sup X) = f by A2, A3, YELLOW_0: 30;

      hence thesis by A1;

    end;

    theorem :: YELLOW16:34

    

     Th33: for I be non empty set holds for J be Poset-yielding non-Empty ManySortedSet of I holds for X be Subset of ( product J) st ex_inf_of (X,( product J)) holds for i be Element of I holds (( inf X) . i) = ( inf ( pi (X,i)))

    proof

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      let X be Subset of ( product J);

      assume ex_inf_of (X,( product J));

      then for i be Element of I holds ex_inf_of (( pi (X,i)),(J . i)) by Th31;

      then

      consider f be Element of ( product J) such that

       A1: for i be Element of I holds (f . i) = ( inf ( pi (X,i))) and

       A2: f is_<=_than X and

       A3: for g be Element of ( product J) st X is_>=_than g holds f >= g by Lm2;

      ( inf X) = f by A2, A3, YELLOW_0: 31;

      hence thesis by A1;

    end;

    theorem :: YELLOW16:35

    

     Th34: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I holds for X be directed Subset of ( product J) holds for i be Element of I holds ( pi (X,i)) is directed

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

      let X be directed Subset of ( product J);

      let i be Element of I;

      let x,y be Element of (J . i);

      assume x in ( pi (X,i));

      then

      consider f be Function such that

       A1: f in X and

       A2: x = (f . i) by CARD_3:def 6;

      assume y in ( pi (X,i));

      then

      consider g be Function such that

       A3: g in X and

       A4: y = (g . i) by CARD_3:def 6;

      reconsider f, g as Element of ( product J) by A1, A3;

      consider h be Element of ( product J) such that

       A5: h in X and

       A6: f <= h and

       A7: g <= h by A1, A3, WAYBEL_0:def 1;

      take (h . i);

      thus (h . i) in ( pi (X,i)) by A5, CARD_3:def 6;

      thus thesis by A2, A4, A6, A7, WAYBEL_3: 28;

    end;

    theorem :: YELLOW16:36

    

     Th35: for I be non empty set holds for J,K be RelStr-yielding non-Empty ManySortedSet of I st for i be Element of I holds (K . i) is SubRelStr of (J . i) holds ( product K) is SubRelStr of ( product J)

    proof

      let I be non empty set;

      let J,K be RelStr-yielding non-Empty ManySortedSet of I such that

       A1: for i be Element of I holds (K . i) is SubRelStr of (J . i);

       A2:

      now

        let i be object;

        assume i in I;

        then

        reconsider j = i as Element of I;

        

         A3: ex R be 1-sorted st R = (J . j) & (( Carrier J) . j) = the carrier of R by PRALG_1:def 15;

        

         A4: ex R be 1-sorted st R = (K . j) & (( Carrier K) . j) = the carrier of R by PRALG_1:def 15;

        (K . j) is SubRelStr of (J . j) by A1;

        hence (( Carrier K) . i) c= (( Carrier J) . i) by A3, A4, YELLOW_0:def 13;

      end;

      

       A5: ( dom ( Carrier K)) = I by PARTFUN1:def 2;

      

       A6: ( dom ( Carrier J)) = I by PARTFUN1:def 2;

      

       A7: the carrier of ( product J) = ( product ( Carrier J)) by YELLOW_1:def 4;

      the carrier of ( product K) = ( product ( Carrier K)) by YELLOW_1:def 4;

      hence

       A8: the carrier of ( product K) c= the carrier of ( product J) by A7, A6, A5, A2, CARD_3: 27;

      let x,y be object;

      assume

       A9: [x, y] in the InternalRel of ( product K);

      reconsider x, y as Element of ( product K) by A9, ZFMISC_1: 87;

      reconsider f = x, g = y as Element of ( product J) by A8;

      

       A10: x <= y by A9, ORDERS_2:def 5;

      now

        let i be Element of I;

        

         A11: (x . i) <= (y . i) by A10, WAYBEL_3: 28;

        (K . i) is SubRelStr of (J . i) by A1;

        hence (f . i) <= (g . i) by A11, YELLOW_0: 59;

      end;

      then f <= g by WAYBEL_3: 28;

      hence thesis by ORDERS_2:def 5;

    end;

    theorem :: YELLOW16:37

    

     Th36: for I be non empty set holds for J,K be RelStr-yielding non-Empty ManySortedSet of I st for i be Element of I holds (K . i) is full SubRelStr of (J . i) holds ( product K) is full SubRelStr of ( product J)

    proof

      let I be non empty set;

      let J,K be RelStr-yielding non-Empty ManySortedSet of I;

      assume

       A1: for i be Element of I holds (K . i) is full SubRelStr of (J . i);

      then for i be Element of I holds (K . i) is SubRelStr of (J . i);

      then

      reconsider S = ( product K) as non empty SubRelStr of ( product J) by Th35;

      

       A2: (the InternalRel of ( product J) |_2 the carrier of S) = (the InternalRel of ( product J) /\ [:the carrier of S, the carrier of S:]) by WELLORD1:def 6;

      S is full

      proof

        the InternalRel of S c= the InternalRel of ( product J) by YELLOW_0:def 13;

        hence the InternalRel of S c= (the InternalRel of ( product J) |_2 the carrier of S) by A2, XBOOLE_1: 19;

        let x,y be object;

        assume

         A3: [x, y] in (the InternalRel of ( product J) |_2 the carrier of S);

        then

         A4: [x, y] in the InternalRel of ( product J) by A2, XBOOLE_0:def 4;

         [x, y] in [:the carrier of S, the carrier of S:] by A2, A3, XBOOLE_0:def 4;

        then

        reconsider x, y as Element of S by ZFMISC_1: 87;

        reconsider a = x, b = y as Element of ( product J) by YELLOW_0: 58;

        reconsider x, y as Element of ( product K);

        

         A5: a <= b by A4, ORDERS_2:def 5;

        now

          let i be Element of I;

          

           A6: (K . i) is full SubRelStr of (J . i) by A1;

          (a . i) <= (b . i) by A5, WAYBEL_3: 28;

          hence (x . i) <= (y . i) by A6, YELLOW_0: 60;

        end;

        then x <= y by WAYBEL_3: 28;

        hence thesis by ORDERS_2:def 5;

      end;

      hence thesis;

    end;

    theorem :: YELLOW16:38

    for L be non empty RelStr, S be non empty SubRelStr of L, X be set holds (S |^ X) is SubRelStr of (L |^ X)

    proof

      let L be non empty RelStr, S be non empty SubRelStr of L, X be set;

      per cases ;

        suppose

         A1: X = {} ;

        then

         A2: (L |^ X) = RelStr (# { {} }, ( id { {} }) #) by YELLOW_1: 27;

        (S |^ X) = RelStr (# { {} }, ( id { {} }) #) by A1, YELLOW_1: 27;

        hence thesis by A2, YELLOW_6: 6;

      end;

        suppose X <> {} ;

        then

        reconsider X as non empty set;

        for i be Element of X holds ((X --> S) . i) is SubRelStr of ((X --> L) . i);

        hence thesis by Th35;

      end;

    end;

    theorem :: YELLOW16:39

    

     Th38: for L be non empty RelStr, S be full non empty SubRelStr of L, X be set holds (S |^ X) is full SubRelStr of (L |^ X)

    proof

      let L be non empty RelStr, S be full non empty SubRelStr of L, X be set;

      per cases ;

        suppose

         A1: X = {} ;

        then

         A2: (L |^ X) = RelStr (# { {} }, ( id { {} }) #) by YELLOW_1: 27;

        (S |^ X) = RelStr (# { {} }, ( id { {} }) #) by A1, YELLOW_1: 27;

        hence thesis by A2, YELLOW_6: 6;

      end;

        suppose X <> {} ;

        then

        reconsider X as non empty set;

        for i be Element of X holds ((X --> S) . i) is full SubRelStr of ((X --> L) . i);

        hence thesis by Th36;

      end;

    end;

    begin

    definition

      let S,T be non empty RelStr, X be set;

      :: YELLOW16:def6

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

      :: YELLOW16:def7

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

    end

    theorem :: YELLOW16:40

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

    theorem :: YELLOW16:41

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

    scheme :: YELLOW16:sch1

    ProductSupsInheriting { I() -> non empty set , J,K() -> Poset-yielding non-Empty ManySortedSet of I() , P[ set, set] } :

for X be Subset of ( product K()) st P[X, ( product K())] holds ( product K()) inherits_sup_of (X,( product J()))

      provided

       A1: for X be Subset of ( product K()) st P[X, ( product K())] holds for i be Element of I() holds P[( pi (X,i)), (K() . i)]

       and

       A2: for i be Element of I() holds (K() . i) is full SubRelStr of (J() . i)

       and

       A3: for i be Element of I(), X be Subset of (K() . i) st P[X, (K() . i)] holds (K() . i) inherits_sup_of (X,(J() . i));

      let X be Subset of ( product K()) such that

       A4: P[X, ( product K())] and

       A5: ex_sup_of (X,( product J()));

      ( product K()) is SubRelStr of ( product J()) by A2, Th36;

      then the carrier of ( product K()) c= the carrier of ( product J()) by YELLOW_0:def 13;

      then

      reconsider Y = X as Subset of ( product J()) by XBOOLE_1: 1;

      set f = ( "\/" (X,( product J())));

       A6:

      now

        let i be Element of I();

        

         A7: ex_sup_of (( pi (Y,i)),(J() . i)) by A5, Th30;

        (K() . i) inherits_sup_of (( pi (X,i)),(J() . i)) by A1, A3, A4;

        then ( sup ( pi (Y,i))) in the carrier of (K() . i) by A7;

        hence (f . i) is Element of (K() . i) by A5, Th32;

      end;

      ( dom f) = I() by WAYBEL_3: 27;

      then ( "\/" (X,( product J()))) is Element of ( product K()) by A6, WAYBEL_3: 27;

      hence thesis;

    end;

    scheme :: YELLOW16:sch2

    PowerSupsInheriting { I() -> non empty set , L() -> non empty Poset , S() -> non empty full SubRelStr of L() , P[ set, set] } :

for X be Subset of (S() |^ I()) st P[X, (S() |^ I())] holds (S() |^ I()) inherits_sup_of (X,(L() |^ I()))

      provided

       A1: for X be Subset of (S() |^ I()) st P[X, (S() |^ I())] holds for i be Element of I() holds P[( pi (X,i)), S()]

       and

       A2: for X be Subset of S() st P[X, S()] holds S() inherits_sup_of (X,L());

      reconsider K = (I() --> S()), J = (I() --> L()) as Poset-yielding non-Empty ManySortedSet of I();

      

       A3: for X be Subset of ( product K) st P[X, ( product K)] holds for i be Element of I() holds P[( pi (X,i)), (K . i)] by A1;

      

       A5: for i be Element of I(), X be Subset of (K . i) st P[X, (K . i)] holds (K . i) inherits_sup_of (X,(J . i)) by A2;

      

       A8: for i be Element of I() holds (K . i) is full SubRelStr of (J . i);

      for X be Subset of ( product K) st P[X, ( product K)] holds ( product K) inherits_sup_of (X,( product J)) from ProductSupsInheriting( A3, A8, A5);

      hence thesis;

    end;

    scheme :: YELLOW16:sch3

    ProductInfsInheriting { I() -> non empty set , J,K() -> Poset-yielding non-Empty ManySortedSet of I() , P[ set, set] } :

for X be Subset of ( product K()) st P[X, ( product K())] holds ( product K()) inherits_inf_of (X,( product J()))

      provided

       A1: for X be Subset of ( product K()) st P[X, ( product K())] holds for i be Element of I() holds P[( pi (X,i)), (K() . i)]

       and

       A2: for i be Element of I() holds (K() . i) is full SubRelStr of (J() . i)

       and

       A3: for i be Element of I(), X be Subset of (K() . i) st P[X, (K() . i)] holds (K() . i) inherits_inf_of (X,(J() . i));

      let X be Subset of ( product K()) such that

       A4: P[X, ( product K())] and

       A5: ex_inf_of (X,( product J()));

      ( product K()) is SubRelStr of ( product J()) by A2, Th36;

      then the carrier of ( product K()) c= the carrier of ( product J()) by YELLOW_0:def 13;

      then

      reconsider Y = X as Subset of ( product J()) by XBOOLE_1: 1;

      set f = ( "/\" (X,( product J())));

       A6:

      now

        let i be Element of I();

        

         A7: ex_inf_of (( pi (Y,i)),(J() . i)) by A5, Th31;

        (K() . i) inherits_inf_of (( pi (X,i)),(J() . i)) by A1, A3, A4;

        then ( inf ( pi (Y,i))) in the carrier of (K() . i) by A7;

        hence (f . i) is Element of (K() . i) by A5, Th33;

      end;

      ( dom f) = I() by WAYBEL_3: 27;

      then ( "/\" (X,( product J()))) is Element of ( product K()) by A6, WAYBEL_3: 27;

      hence thesis;

    end;

    scheme :: YELLOW16:sch4

    PowerInfsInheriting { I() -> non empty set , L() -> non empty Poset , S() -> non empty full SubRelStr of L() , P[ set, set] } :

for X be Subset of (S() |^ I()) st P[X, (S() |^ I())] holds (S() |^ I()) inherits_inf_of (X,(L() |^ I()))

      provided

       A1: for X be Subset of (S() |^ I()) st P[X, (S() |^ I())] holds for i be Element of I() holds P[( pi (X,i)), S()]

       and

       A2: for X be Subset of S() st P[X, S()] holds S() inherits_inf_of (X,L());

      reconsider K = (I() --> S()), J = (I() --> L()) as Poset-yielding non-Empty ManySortedSet of I();

      

       A3: for X be Subset of ( product K) st P[X, ( product K)] holds for i be Element of I() holds P[( pi (X,i)), (K . i)] by A1;

      

       A5: for i be Element of I(), X be Subset of (K . i) st P[X, (K . i)] holds (K . i) inherits_inf_of (X,(J . i)) by A2;

      

       A8: for i be Element of I() holds (K . i) is full SubRelStr of (J . i);

      for X be Subset of ( product K) st P[X, ( product K)] holds ( product K) inherits_inf_of (X,( product J)) from ProductInfsInheriting( A3, A8, A5);

      hence thesis;

    end;

    registration

      let I be set;

      let L be non empty RelStr;

      let X be non empty Subset of (L |^ I);

      let i be set;

      cluster ( pi (X,i)) -> non empty;

      coherence

      proof

        reconsider Y = X as non empty Subset of ( product (I --> L));

        set f = the Element of Y;

        reconsider f as Function;

        (f . i) in ( pi (X,i)) by CARD_3:def 6;

        hence thesis;

      end;

    end

    theorem :: YELLOW16:42

    for L be non empty Poset holds for S be directed-sups-inheriting non empty full SubRelStr of L holds for X be non empty set holds (S |^ X) is directed-sups-inheriting SubRelStr of (L |^ X)

    proof

      let L be non empty Poset;

      let S be directed-sups-inheriting non empty full SubRelStr of L;

      let X be non empty set;

      reconsider SX = (S |^ X) as full non empty SubRelStr of (L |^ X) by Th38;

      defpred P[ set, non empty reflexive RelStr] means $1 is directed non empty Subset of $2;

       A1:

      now

        let A be Subset of (S |^ X);

        assume P[A, (S |^ X)];

        then

        reconsider B = A as directed non empty Subset of (S |^ X);

        let i be Element of X;

        ((X --> S) . i) = S;

        then ( pi (B,i)) is directed non empty Subset of S by Th34;

        hence P[( pi (A,i)), S];

      end;

       A2:

      now

        let X be Subset of S;

        assume P[X, S];

        then ex_sup_of (X,L) implies ex_sup_of (X,S) & ( sup X) = ( "\/" (X,L)) by WAYBEL_0: 7;

        hence S inherits_sup_of (X,L);

      end;

      SX is directed-sups-inheriting

      proof

        let A be directed Subset of SX;

        for A be Subset of (S |^ X) st P[A, (S |^ X)] holds (S |^ X) inherits_sup_of (A,(L |^ X)) from PowerSupsInheriting( A1, A2);

        then A <> {} implies (S |^ X) inherits_sup_of (A,(L |^ X));

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      let I be non empty set;

      let J be RelStr-yielding non-Empty ManySortedSet of I;

      let X be non empty Subset of ( product J);

      let i be set;

      cluster ( pi (X,i)) -> non empty;

      coherence

      proof

        set f = the Element of X;

        reconsider f as Function;

        (f . i) in ( pi (X,i)) by CARD_3:def 6;

        hence thesis;

      end;

    end

    theorem :: YELLOW16:43

    

     Th42: for X be non empty set holds for L be up-complete non empty Poset holds (L |^ X) is up-complete

    proof

      let X be non empty set;

      let L be up-complete non empty Poset;

      now

        let A be non empty directed Subset of (L |^ X);

        reconsider B = A as non empty directed Subset of ( product (X --> L));

        now

          let x be Element of X;

          ( pi (B,x)) is directed non empty by Th34;

          hence ex_sup_of (( pi (A,x)),((X --> L) . x)) by WAYBEL_0: 75;

        end;

        hence ex_sup_of (A,(L |^ X)) by Th30;

      end;

      hence thesis by WAYBEL_0: 75;

    end;

    registration

      let L be up-complete non empty Poset;

      let X be non empty set;

      cluster (L |^ X) -> up-complete;

      coherence by Th42;

    end

    begin

    theorem :: YELLOW16:44

    

     Th43: for T be non empty TopSpace, S be non empty SubSpace of T holds for f be Function of T, S st f is being_a_retraction holds ( rng f) = the carrier of S

    proof

      let T be non empty TopSpace, S be non empty SubSpace of T;

      let f be Function of T, S such that

       A1: for W be Point of T st W in the carrier of S holds (f . W) = W;

      thus ( rng f) c= the carrier of S;

      let x be object;

      

       A2: ( [#] S) = the carrier of S;

      ( [#] T) = the carrier of T;

      then

       A3: the carrier of S c= the carrier of T by A2, PRE_TOPC:def 4;

      assume

       A4: x in the carrier of S;

      then x in the carrier of T by A3;

      then

       A5: x in ( dom f) by FUNCT_2:def 1;

      (f . x) = x by A1, A3, A4;

      hence thesis by A5, FUNCT_1:def 3;

    end;

    theorem :: YELLOW16:45

    for T be non empty TopSpace, S be non empty SubSpace of T holds for f be continuous Function of T, S st f is being_a_retraction holds f is idempotent

    proof

      let T be non empty TopSpace, S be non empty SubSpace of T;

      

       A1: ( [#] S) = the carrier of S;

      let f be continuous Function of T, S such that

       A2: f is being_a_retraction;

      

       A3: ( rng f) = the carrier of S by A2, Th43;

      

       A4: ( dom f) = the carrier of T by FUNCT_2:def 1;

      ( [#] T) = the carrier of T;

      then

       A5: the carrier of S c= the carrier of T by A1, PRE_TOPC:def 4;

       A6:

      now

        let x be object;

        assume

         A7: x in the carrier of T;

        then

         A8: (f . x) in ( rng f) by A4, FUNCT_1:def 3;

        ((f * f) . x) = (f . (f . x)) by A4, A7, FUNCT_1: 13;

        hence ((f * f) . x) = (f . x) by A2, A5, A3, A8;

      end;

      ( dom (f * f)) = the carrier of T by A5, A4, A3, RELAT_1: 27;

      then (f * f) = f by A4, A6, FUNCT_1: 2;

      hence thesis by QUANTAL1:def 9;

    end;

    theorem :: YELLOW16:46

    

     Th45: for T be non empty TopSpace, V be open Subset of T holds ( chi (V,the carrier of T)) is continuous Function of T, Sierpinski_Space

    proof

      let T be non empty TopSpace, V be open Subset of T;

      reconsider c = ( chi (V,the carrier of T)) as Function of T, Sierpinski_Space by WAYBEL18:def 9;

      

       A1: (c " { 0 , 1}) = ( [#] T) by FUNCT_2: 40;

      c = ( chi ((c " {1}),the carrier of T)) by FUNCT_3: 40;

      then

       A2: V = (c " {1}) by FUNCT_3: 38;

      

       A3: (c " {} ) = ( {} T);

       A4:

      now

        let W be Subset of Sierpinski_Space ;

        assume W is open;

        then W in the topology of Sierpinski_Space by PRE_TOPC:def 2;

        then W in { {} , {1}, { 0 , 1}} by WAYBEL18:def 9;

        hence (c " W) is open by A2, A3, A1, ENUMSET1:def 1;

      end;

      ( [#] Sierpinski_Space ) <> {} ;

      hence thesis by A4, TOPS_2: 43;

    end;

    theorem :: YELLOW16:47

    for T be non empty TopSpace, x,y be Element of T st for W be open Subset of T st y in W holds x in W holds (( 0 ,1) --> (y,x)) is continuous Function of Sierpinski_Space , T

    proof

      let T be non empty TopSpace;

      let x,y be Element of T such that

       A1: for W be open Subset of T st y in W holds x in W;

      

       A2: the carrier of Sierpinski_Space = { 0 , { 0 }} by WAYBEL18:def 9, CARD_1: 49;

      then

      reconsider i = (( 0 , { 0 }) --> (y,x)) as Function of Sierpinski_Space , T;

      

       A3: (i . 1) = x by FUNCT_4: 63, CARD_1: 49;

      

       A4: not 1 in { 0 } by TARSKI:def 1;

      

       A5: 0 in { 0 } by TARSKI:def 1;

      

       A6: 1 in { 0 , 1} by TARSKI:def 2;

      

       A7: (i . 0 ) = y by FUNCT_4: 63;

       A8:

      now

        let W be Subset of T;

        assume W is open;

        then

         A9: y in W & x in W or not y in W & x in W or not y in W & not x in W by A1;

        

         A10: (i " W) = {} or (i " W) = { 0 } or (i " W) = {1} or (i " W) = { 0 , 1} by A2, ZFMISC_1: 36, CARD_1: 49;

        (i " W) <> { 0 } by A7, A3, A6, A5, A4, A9, FUNCT_2: 38, CARD_1: 49;

        then (i " W) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1, A10;

        then (i " W) in the topology of Sierpinski_Space by WAYBEL18:def 9;

        hence (i " W) is open by PRE_TOPC:def 2;

      end;

      ( [#] T) <> {} ;

      hence thesis by A8, TOPS_2: 43, CARD_1: 49;

    end;

    theorem :: YELLOW16:48

    for T be non empty TopSpace, x,y be Element of T holds for V be open Subset of T st x in V & not y in V holds (( chi (V,the carrier of T)) * (( 0 ,1) --> (y,x))) = ( id Sierpinski_Space )

    proof

      let T be non empty TopSpace;

      let x,y be Element of T, V be open Subset of T such that

       A1: x in V and

       A2: not y in V;

      reconsider c = ( chi (V,the carrier of T)) as Function of T, Sierpinski_Space by Th45;

      

       A3: (c . x) = 1 by A1, FUNCT_3:def 3;

      

       A4: the carrier of Sierpinski_Space = { 0 , { 0 }} by WAYBEL18:def 9, CARD_1: 49;

      then

      reconsider i = (( 0 , { 0 }) --> (y,x)) as Function of Sierpinski_Space , T;

      

       A5: (i . 1) = x by FUNCT_4: 63, CARD_1: 49;

      

       A6: (c . y) = 0 by A2, FUNCT_3:def 3;

      

       A7: (i . 0 ) = y by FUNCT_4: 63;

      now

        thus (c * i) is Function of Sierpinski_Space , Sierpinski_Space ;

        let a be Element of Sierpinski_Space ;

        a = 0 or a = 1 by A4, TARSKI:def 2, CARD_1: 49;

        

        hence ((c * i) . a) = a by A7, A5, A3, A6, FUNCT_2: 15

        .= (( id Sierpinski_Space ) . a);

      end;

      hence thesis by FUNCT_2: 63, CARD_1: 49;

    end;

    theorem :: YELLOW16:49

    for T be non empty 1-sorted, V,W be Subset of T holds for S be TopAugmentation of ( BoolePoset { 0 }) holds for f,g be Function of T, S st f = ( chi (V,the carrier of T)) & g = ( chi (W,the carrier of T)) holds V c= W iff f <= g

    proof

      let T be non empty 1-sorted, V,W be Subset of T;

      let S be TopAugmentation of ( BoolePoset { 0 });

      let c1,c2 be Function of T, S such that

       A1: c1 = ( chi (V,the carrier of T)) and

       A2: c2 = ( chi (W,the carrier of T));

      

       A3: the RelStr of S = ( BoolePoset { 0 }) by YELLOW_9:def 4;

      hereby

        assume

         A4: V c= W;

        now

          let z be set;

          assume z in the carrier of T;

          then

          reconsider x = z as Element of T;

          reconsider a = (c1 . x), b = (c2 . x) as Element of ( BoolePoset { 0 }) by A3;

          x in V & x in W or not x in V by A4;

          then (c1 . x) = 1 & (c2 . x) = 1 or (c1 . x) = 0 by A1, A2, FUNCT_3:def 3;

          then (c1 . x) c= (c2 . x);

          then a <= b by YELLOW_1: 2;

          hence ex a,b be Element of S st a = (c1 . z) & b = (c2 . z) & a <= b by A3, YELLOW_0: 1;

        end;

        hence c1 <= c2;

      end;

      assume

       A5: c1 <= c2;

      let x be object;

      assume that

       A6: x in V and

       A7: not x in W;

      reconsider x as Element of T by A6;

      

       A8: (c2 . x) = 0 by A2, A7, FUNCT_3:def 3;

      

       A9: 0 c= { 0 };

      reconsider a = (c1 . x), b = (c2 . x) as Element of ( BoolePoset { 0 }) by A3;

      ex a,b be Element of S st a = (c1 . x) & b = (c2 . x) & a <= b by A5;

      then

       A10: a <= b by A3, YELLOW_0: 1;

      (c1 . x) = 1 by A1, A6, FUNCT_3:def 3;

      then { 0 } c= 0 by A8, A10, YELLOW_1: 2, CARD_1: 49;

      hence thesis by A9, XBOOLE_0:def 10;

    end;

    theorem :: YELLOW16:50

    for L be non empty RelStr, X be non empty set holds for R be full non empty SubRelStr of (L |^ X) st for a be set holds a is Element of R iff ex x be Element of L st a = (X --> x) holds (L,R) are_isomorphic

    proof

      let L be non empty RelStr, X be non empty set;

      deffunc F( set) = (X --> $1);

      consider f be ManySortedSet of the carrier of L such that

       A1: for i be Element of L holds (f . i) = F(i) from PBOOLE:sch 5;

      let R be full non empty SubRelStr of (L |^ X) such that

       A2: for a be set holds a is Element of R iff ex x be Element of L st a = (X --> x);

      

       A3: ( rng f) c= the carrier of R

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A4: x in ( dom f) and

         A5: y = (f . x) by FUNCT_1:def 3;

        reconsider x as Element of L by A4;

        y = (X --> x) by A1, A5;

        then y is Element of R by A2;

        hence thesis;

      end;

      

       A6: ( dom f) = the carrier of L by PARTFUN1:def 2;

      then

      reconsider f as Function of L, R by A3, FUNCT_2: 2;

      

       A7: f is one-to-one

      proof

        let x,y be Element of L;

        (f . y) = (X --> y) by A1;

        then

         A8: (f . y) = [:X, {y}:] by FUNCOP_1:def 2;

        (f . x) = (X --> x) by A1;

        then (f . x) = [:X, {x}:] by FUNCOP_1:def 2;

        then (f . x) = (f . y) implies {x} = {y} by A8, ZFMISC_1: 110;

        hence thesis by ZFMISC_1: 3;

      end;

       A9:

      now

        set i = the Element of X;

        let x,y be Element of L;

        reconsider a = (f . x), b = (f . y) as Element of (L |^ X) by YELLOW_0: 58;

        reconsider Xx = (X --> x), Xy = (X --> y) as Function of X, L;

        reconsider a9 = a, b9 = b as Element of ( product (X --> L));

        

         A11: (f . y) = (X --> y) by A1;

        

         A12: (f . x) = (X --> x) by A1;

        hereby

          assume

           A13: x <= y;

          Xx <= Xy

          proof

            let i be set;

            assume

             A14: i in X;

            then

             A15: ((X --> y) . i) = y by FUNCOP_1: 7;

            ((X --> x) . i) = x by A14, FUNCOP_1: 7;

            hence thesis by A13, A15;

          end;

          then a <= b by A12, A11, WAYBEL10: 11;

          hence (f . x) <= (f . y) by YELLOW_0: 60;

        end;

        assume (f . x) <= (f . y);

        then a <= b by YELLOW_0: 59;

        then (a9 . i) <= (b9 . i) by WAYBEL_3: 28;

        then x <= (Xy . i) by A12, A11;

        hence x <= y;

      end;

      take f;

      ( rng f) = the carrier of R

      proof

        thus ( rng f) c= the carrier of R;

        let x be object;

        assume x in the carrier of R;

        then

        reconsider a = x as Element of R;

        consider i be Element of L such that

         A16: a = (X --> i) by A2;

        a = (f . i) by A1, A16;

        hence thesis by A6, FUNCT_1:def 3;

      end;

      hence thesis by A7, A9, WAYBEL_0: 66;

    end;

    theorem :: YELLOW16:51

    for S,T be non empty TopSpace holds (S,T) are_homeomorphic iff ex f be continuous Function of S, T, g be continuous Function of T, S st (f * g) = ( id T) & (g * f) = ( id S)

    proof

      let S,T be non empty TopSpace;

      hereby

        assume (S,T) are_homeomorphic ;

        then

        consider f be Function of S, T such that

         A1: f is being_homeomorphism;

        reconsider f as continuous Function of S, T by A1, TOPS_2:def 5;

        

         A2: ( rng f) = ( [#] T) by A1, TOPS_2:def 5;

        reconsider g = (f " ) as continuous Function of T, S by A1, TOPS_2:def 5;

        take f, g;

        

         A3: ( dom f) = ( [#] S) by A1, TOPS_2:def 5;

        f is one-to-one by A1, TOPS_2:def 5;

        hence (f * g) = ( id T) & (g * f) = ( id S) by A2, A3, TOPS_2: 52;

      end;

      given f be continuous Function of S, T, g be continuous Function of T, S such that

       A4: (f * g) = ( id T) and

       A5: (g * f) = ( id S);

      

       A6: f is onto by A4, FUNCT_2: 23;

      then

       A7: ( rng f) = ( [#] T) by FUNCT_2:def 3;

      take f;

      

       A8: ( dom f) = ( [#] S) by FUNCT_2:def 1;

      

       A9: f is one-to-one by A5, FUNCT_2: 23;

      

      then g = (f qua Function " ) by A5, A7, FUNCT_2: 30

      .= (f " ) by A6, A9, TOPS_2:def 4;

      hence thesis by A9, A7, A8, TOPS_2:def 5;

    end;

    theorem :: YELLOW16:52

    

     Th51: for T,S,R be non empty TopSpace holds for f be Function of T, S, g be Function of S, T, h be Function of S, R st (f * g) = ( id S) & h is being_homeomorphism holds ((h * f) * (g * (h " ))) = ( id R)

    proof

      let T,S,R be non empty TopSpace;

      let f be Function of T, S, g be Function of S, T, h be Function of S, R such that

       A1: (f * g) = ( id S) and

       A2: h is being_homeomorphism;

      

       A3: h is one-to-one by A2, TOPS_2:def 5;

      

       A4: ( rng h) = ( [#] R) by A2, TOPS_2:def 5;

      

      thus ((h * f) * (g * (h " ))) = (((h * f) * g) * (h " )) by RELAT_1: 36

      .= ((h * ( id the carrier of S)) * (h " )) by A1, RELAT_1: 36

      .= (h * (h " )) by FUNCT_2: 17

      .= ( id R) by A3, A4, TOPS_2: 52;

    end;

    theorem :: YELLOW16:53

    

     Th52: for T,S,R be non empty TopSpace st S is_Retract_of T & (S,R) are_homeomorphic holds R is_Retract_of T

    proof

      let T,S,R be non empty TopSpace;

      given f be continuous Function of S, T, g be continuous Function of T, S such that

       A1: (g * f) = ( id S);

      given h be Function of S, R such that

       A2: h is being_homeomorphism;

      (h " ) is continuous by A2, TOPS_2:def 5;

      then

      reconsider f9 = (f * (h " )) as continuous Function of R, T;

      h is continuous by A2, TOPS_2:def 5;

      then

      reconsider g9 = (h * g) as continuous Function of T, R;

      take f9, g9;

      thus thesis by A1, A2, Th51;

    end;

    theorem :: YELLOW16:54

    

     Th53: for T be non empty TopSpace, S be non empty SubSpace of T holds ( incl (S,T)) is continuous

    proof

      let T be non empty TopSpace, S be non empty SubSpace of T;

      ( incl (S,T)) = ( id S) by BORSUK_1: 1, YELLOW_9:def 1;

      hence thesis by PRE_TOPC: 26;

    end;

    theorem :: YELLOW16:55

    

     Th54: for T be non empty TopSpace holds for S be non empty SubSpace of T, f be continuous Function of T, S st f is being_a_retraction holds (f * ( incl (S,T))) = ( id S)

    proof

      let T be non empty TopSpace, S be non empty SubSpace of T;

      let f be continuous Function of T, S such that

       A1: f is being_a_retraction;

      

       A2: ( [#] S) = the carrier of S;

      ( [#] T) = the carrier of T;

      then

       A3: the carrier of S c= the carrier of T by A2, PRE_TOPC:def 4;

      then

       A4: ( incl (S,T)) = ( id the carrier of S) by YELLOW_9:def 1;

      now

        let x be Element of S;

        reconsider y = x as Point of T by A3;

        

        thus ((f * ( incl (S,T))) . x) = (f . (( incl (S,T)) . x)) by FUNCT_2: 15

        .= (f . x) by A4

        .= y by A1

        .= (( id S) . x);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: YELLOW16:56

    

     Th55: for T be non empty TopSpace, S be non empty SubSpace of T st S is_a_retract_of T holds S is_Retract_of T

    proof

      let T be non empty TopSpace, S be non empty SubSpace of T;

      reconsider g = ( incl (S,T)) as continuous Function of S, T by Th53;

      given f be continuous Function of T, S such that

       A1: f is being_a_retraction;

      take g, f;

      thus thesis by A1, Th54;

    end;

    theorem :: YELLOW16:57

    for R,T be non empty TopSpace holds R is_Retract_of T iff ex S be non empty SubSpace of T st S is_a_retract_of T & (S,R) are_homeomorphic

    proof

      let R,T be non empty TopSpace;

      hereby

        assume R is_Retract_of T;

        then

        consider f be Function of T, T such that

         A1: f is continuous and

         A2: (f * f) = f and

         A3: (( Image f),R) are_homeomorphic by WAYBEL18:def 8;

        reconsider S = ( Image f) as non empty SubSpace of T;

        f = ( corestr f) by WAYBEL18:def 7;

        then

        reconsider f as continuous Function of T, S by A1, WAYBEL18: 10;

        take S;

        

         A4: ( [#] T) = the carrier of T;

        ( [#] S) = the carrier of S;

        then the carrier of S c= the carrier of T by A4, PRE_TOPC:def 4;

        then

        reconsider rf = ( rng f) as Subset of T by XBOOLE_1: 1;

        now

          let x be Point of T;

          assume x in the carrier of S;

          then x in ( [#] (T | rf)) by WAYBEL18:def 6;

          then x in ( rng f) by PRE_TOPC:def 5;

          then ex y be object st y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

          hence (f . x) = x by A2, FUNCT_1: 13;

        end;

        then f is being_a_retraction;

        hence S is_a_retract_of T & (S,R) are_homeomorphic by A3;

      end;

      given S be non empty SubSpace of T such that

       A5: S is_a_retract_of T and

       A6: (S,R) are_homeomorphic ;

      thus thesis by A5, A6, Th52, Th55;

    end;