waybel20.miz



    begin

    theorem :: WAYBEL20:1

    

     Th1: for X be set, S be Subset of ( id X) holds ( proj1 S) = ( proj2 S)

    proof

      let X be set, S be Subset of ( id X);

      now

        let x be object;

        hereby

          assume x in ( proj1 S);

          then

          consider y be object such that

           A1: [x, y] in S by XTUPLE_0:def 12;

          x = y by A1, RELAT_1:def 10;

          hence x in ( proj2 S) by A1, XTUPLE_0:def 13;

        end;

        assume x in ( proj2 S);

        then

        consider y be object such that

         A2: [y, x] in S by XTUPLE_0:def 13;

        x = y by A2, RELAT_1:def 10;

        hence x in ( proj1 S) by A2, XTUPLE_0:def 12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL20:2

    

     Th2: for X,Y be non empty set, f be Function of X, Y holds ( [:f, f:] " ( id Y)) is Equivalence_Relation of X

    proof

      let X,Y be non empty set, f be Function of X, Y;

      set ff = ( [:f, f:] " ( id Y));

      

       A1: ( dom f) = X by FUNCT_2:def 1;

      reconsider R9 = ff as Relation of X;

      

       A2: ( dom [:f, f:]) = [:( dom f), ( dom f):] by FUNCT_3:def 8;

      R9 is_reflexive_in X

      proof

        let x be object;

        assume

         A3: x in X;

        then

        reconsider x9 = x as Element of X;

        

         A4: [(f . x9), (f . x9)] in ( id Y) by RELAT_1:def 10;

         [x, x] in ( dom [:f, f:]) & [(f . x), (f . x)] = ( [:f, f:] . (x,x)) by A2, A1, A3, FUNCT_3:def 8, ZFMISC_1:def 2;

        hence thesis by A4, FUNCT_1:def 7;

      end;

      then

       A5: ( dom R9) = X & ( field R9) = X by ORDERS_1: 13;

      

       A6: R9 is_symmetric_in X

      proof

        let x,y be object;

        assume that

         A7: x in X & y in X and

         A8: [x, y] in R9;

        reconsider x9 = x, y9 = y as Element of X by A7;

        

         A9: [y, x] in ( dom [:f, f:]) & [(f . y), (f . x)] = ( [:f, f:] . (y,x)) by A2, A1, A7, FUNCT_3:def 8, ZFMISC_1:def 2;

        

         A10: ( [:f, f:] . [x, y]) in ( id Y) & [(f . x), (f . y)] = ( [:f, f:] . (x,y)) by A1, A7, A8, FUNCT_1:def 7, FUNCT_3:def 8;

        then (f . x9) = (f . y9) by RELAT_1:def 10;

        hence thesis by A10, A9, FUNCT_1:def 7;

      end;

      R9 is_transitive_in X

      proof

        let x,y,z be object such that

         A11: x in X and

         A12: y in X and

         A13: z in X and

         A14: [x, y] in R9 and

         A15: [y, z] in R9;

        

         A16: [x, z] in ( dom [:f, f:]) & [(f . x), (f . z)] = ( [:f, f:] . (x,z)) by A2, A1, A11, A13, FUNCT_3:def 8, ZFMISC_1:def 2;

        reconsider y9 = y, z9 = z as Element of X by A12, A13;

        ( [:f, f:] . [y, z]) in ( id Y) & [(f . y), (f . z)] = ( [:f, f:] . (y,z)) by A1, A12, A13, A15, FUNCT_1:def 7, FUNCT_3:def 8;

        then

         A17: (f . y9) = (f . z9) by RELAT_1:def 10;

        ( [:f, f:] . [x, y]) in ( id Y) & [(f . x), (f . y)] = ( [:f, f:] . (x,y)) by A1, A11, A12, A14, FUNCT_1:def 7, FUNCT_3:def 8;

        hence thesis by A17, A16, FUNCT_1:def 7;

      end;

      hence thesis by A5, A6, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

    end;

    definition

      let L1,L2,T1,T2 be RelStr, f be Function of L1, T1, g be Function of L2, T2;

      :: original: [:

      redefine

      func [:f,g:] -> Function of [:L1, L2:], [:T1, T2:] ;

      coherence

      proof

        the carrier of [:L1, L2:] = [:the carrier of L1, the carrier of L2:] & the carrier of [:T1, T2:] = [:the carrier of T1, the carrier of T2:] by YELLOW_3:def 2;

        hence [:f, g:] is Function of [:L1, L2:], [:T1, T2:];

      end;

    end

    theorem :: WAYBEL20:3

    

     Th3: for f,g be Function, X be set holds ( proj1 ( [:f, g:] .: X)) c= (f .: ( proj1 X)) & ( proj2 ( [:f, g:] .: X)) c= (g .: ( proj2 X))

    proof

      let f,g be Function, X be set;

      

       A1: ( dom [:f, g:]) = [:( dom f), ( dom g):] by FUNCT_3:def 8;

      hereby

        let x be object;

        assume x in ( proj1 ( [:f, g:] .: X));

        then

        consider y be object such that

         A2: [x, y] in ( [:f, g:] .: X) by XTUPLE_0:def 12;

        consider xy be object such that

         A3: xy in ( dom [:f, g:]) and

         A4: xy in X and

         A5: [x, y] = ( [:f, g:] . xy) by A2, FUNCT_1:def 6;

        consider x9,y9 be object such that

         A6: x9 in ( dom f) and

         A7: y9 in ( dom g) and

         A8: xy = [x9, y9] by A1, A3, ZFMISC_1:def 2;

         [x, y] = ( [:f, g:] . (x9,y9)) by A5, A8

        .= [(f . x9), (g . y9)] by A6, A7, FUNCT_3:def 8;

        then

         A9: x = (f . x9) by XTUPLE_0: 1;

        x9 in ( proj1 X) by A4, A8, XTUPLE_0:def 12;

        hence x in (f .: ( proj1 X)) by A6, A9, FUNCT_1:def 6;

      end;

      let y be object;

      assume y in ( proj2 ( [:f, g:] .: X));

      then

      consider x be object such that

       A10: [x, y] in ( [:f, g:] .: X) by XTUPLE_0:def 13;

      consider xy be object such that

       A11: xy in ( dom [:f, g:]) and

       A12: xy in X and

       A13: [x, y] = ( [:f, g:] . xy) by A10, FUNCT_1:def 6;

      consider x9,y9 be object such that

       A14: x9 in ( dom f) and

       A15: y9 in ( dom g) and

       A16: xy = [x9, y9] by A1, A11, ZFMISC_1:def 2;

       [x, y] = ( [:f, g:] . (x9,y9)) by A13, A16

      .= [(f . x9), (g . y9)] by A14, A15, FUNCT_3:def 8;

      then

       A17: y = (g . y9) by XTUPLE_0: 1;

      y9 in ( proj2 X) by A12, A16, XTUPLE_0:def 13;

      hence thesis by A15, A17, FUNCT_1:def 6;

    end;

    theorem :: WAYBEL20:4

    

     Th4: for f,g be Function, X be set st X c= [:( dom f), ( dom g):] holds ( proj1 ( [:f, g:] .: X)) = (f .: ( proj1 X)) & ( proj2 ( [:f, g:] .: X)) = (g .: ( proj2 X))

    proof

      let f,g be Function, X be set such that

       A1: X c= [:( dom f), ( dom g):];

      

       A2: ( dom [:f, g:]) = [:( dom f), ( dom g):] by FUNCT_3:def 8;

      

       A3: ( proj1 ( [:f, g:] .: X)) c= (f .: ( proj1 X)) by Th3;

      now

        let x be object;

        thus x in ( proj1 ( [:f, g:] .: X)) implies x in (f .: ( proj1 X)) by A3;

        assume x in (f .: ( proj1 X));

        then

        consider x9 be object such that

         A4: x9 in ( dom f) and

         A5: x9 in ( proj1 X) and

         A6: x = (f . x9) by FUNCT_1:def 6;

        consider y9 be object such that

         A7: [x9, y9] in X by A5, XTUPLE_0:def 12;

        y9 in ( dom g) by A1, A7, ZFMISC_1: 87;

        then ( [:f, g:] . (x9,y9)) = [(f . x9), (g . y9)] by A4, FUNCT_3:def 8;

        then [x, (g . y9)] in ( [:f, g:] .: X) by A1, A2, A6, A7, FUNCT_1:def 6;

        hence x in ( proj1 ( [:f, g:] .: X)) by XTUPLE_0:def 12;

      end;

      hence ( proj1 ( [:f, g:] .: X)) = (f .: ( proj1 X)) by TARSKI: 2;

      

       A8: ( proj2 ( [:f, g:] .: X)) c= (g .: ( proj2 X)) by Th3;

      now

        let x be object;

        thus x in ( proj2 ( [:f, g:] .: X)) implies x in (g .: ( proj2 X)) by A8;

        assume x in (g .: ( proj2 X));

        then

        consider x9 be object such that

         A9: x9 in ( dom g) and

         A10: x9 in ( proj2 X) and

         A11: x = (g . x9) by FUNCT_1:def 6;

        consider y9 be object such that

         A12: [y9, x9] in X by A10, XTUPLE_0:def 13;

        y9 in ( dom f) by A1, A12, ZFMISC_1: 87;

        then ( [:f, g:] . (y9,x9)) = [(f . y9), (g . x9)] by A9, FUNCT_3:def 8;

        then [(f . y9), x] in ( [:f, g:] .: X) by A1, A2, A11, A12, FUNCT_1:def 6;

        hence x in ( proj2 ( [:f, g:] .: X)) by XTUPLE_0:def 13;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL20:5

    

     Th5: for S be non empty antisymmetric RelStr st ex_inf_of ( {} ,S) holds S is upper-bounded

    proof

      let S be non empty antisymmetric RelStr;

      assume

       A1: ex_inf_of ( {} ,S);

      take ( Top S);

      let x be Element of S;

       {} is_>=_than x;

      hence thesis by A1, YELLOW_0: 31;

    end;

    theorem :: WAYBEL20:6

    

     Th6: for S be non empty antisymmetric RelStr st ex_sup_of ( {} ,S) holds S is lower-bounded

    proof

      let S be non empty antisymmetric RelStr;

      assume

       A1: ex_sup_of ( {} ,S);

      take ( Bottom S);

      let x be Element of S;

       {} is_<=_than x;

      hence thesis by A1, YELLOW_0: 30;

    end;

    theorem :: WAYBEL20:7

    

     Th7: for L1,L2 be antisymmetric non empty RelStr, D be Subset of [:L1, L2:] st ex_inf_of (D, [:L1, L2:]) holds ( inf D) = [( inf ( proj1 D)), ( inf ( proj2 D))]

    proof

      let L1,L2 be antisymmetric non empty RelStr, D be Subset of [:L1, L2:] such that

       A1: ex_inf_of (D, [:L1, L2:]);

      per cases ;

        suppose D <> {} ;

        hence thesis by A1, YELLOW_3: 47;

      end;

        suppose

         A2: D = {} ;

        then ex_inf_of ( {} ,L2) by A1, FUNCT_5: 8, YELLOW_3: 42;

        then

         A3: L2 is upper-bounded by Th5;

         ex_inf_of ( {} ,L1) by A1, A2, FUNCT_5: 8, YELLOW_3: 42;

        then L1 is upper-bounded by Th5;

        hence thesis by A1, A3, YELLOW10: 6;

      end;

    end;

    theorem :: WAYBEL20:8

    

     Th8: for L1,L2 be antisymmetric non empty RelStr, D be Subset of [:L1, L2:] st ex_sup_of (D, [:L1, L2:]) holds ( sup D) = [( sup ( proj1 D)), ( sup ( proj2 D))]

    proof

      let L1,L2 be antisymmetric non empty RelStr, D be Subset of [:L1, L2:] such that

       A1: ex_sup_of (D, [:L1, L2:]);

      per cases ;

        suppose D <> {} ;

        hence thesis by A1, YELLOW_3: 46;

      end;

        suppose

         A2: D = {} ;

        then ex_sup_of ( {} ,L2) by A1, FUNCT_5: 8, YELLOW_3: 41;

        then

         A3: L2 is lower-bounded by Th6;

         ex_sup_of ( {} ,L1) by A1, A2, FUNCT_5: 8, YELLOW_3: 41;

        then L1 is lower-bounded by Th6;

        hence thesis by A1, A3, YELLOW10: 5;

      end;

    end;

    theorem :: WAYBEL20:9

    

     Th9: for L1,L2,T1,T2 be antisymmetric non empty RelStr, f be Function of L1, T1, g be Function of L2, T2 st f is infs-preserving & g is infs-preserving holds [:f, g:] is infs-preserving

    proof

      let L1,L2,T1,T2 be antisymmetric non empty RelStr, f be Function of L1, T1, g be Function of L2, T2 such that

       A1: f is infs-preserving and

       A2: g is infs-preserving;

      let X be Subset of [:L1, L2:];

      

       A3: f preserves_inf_of ( proj1 X) by A1;

      

       A4: g preserves_inf_of ( proj2 X) by A2;

      set iX = ( [:f, g:] .: X);

      

       A5: ( dom f) = the carrier of L1 & ( dom g) = the carrier of L2 by FUNCT_2:def 1;

      assume

       A6: ex_inf_of (X, [:L1, L2:]);

      then

       A7: ex_inf_of (( proj1 X),L1) by YELLOW_3: 42;

      

       A8: ex_inf_of (( proj2 X),L2) by A6, YELLOW_3: 42;

      X c= the carrier of [:L1, L2:];

      then

       A9: X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;

      then

       A10: ( proj2 iX) = (g .: ( proj2 X)) by A5, Th4;

      then

       A11: ex_inf_of (( proj2 iX),T2) by A4, A8;

      

       A12: ( proj1 iX) = (f .: ( proj1 X)) by A5, A9, Th4;

      then ex_inf_of (( proj1 iX),T1) by A3, A7;

      hence ex_inf_of (( [:f, g:] .: X), [:T1, T2:]) by A11, YELLOW_3: 42;

      

      hence ( inf ( [:f, g:] .: X)) = [( inf (f .: ( proj1 X))), ( inf (g .: ( proj2 X)))] by A12, A10, Th7

      .= [(f . ( inf ( proj1 X))), ( inf (g .: ( proj2 X)))] by A3, A7

      .= [(f . ( inf ( proj1 X))), (g . ( inf ( proj2 X)))] by A4, A8

      .= ( [:f, g:] . (( inf ( proj1 X)),( inf ( proj2 X)))) by A5, FUNCT_3:def 8

      .= ( [:f, g:] . ( inf X)) by A6, Th7;

    end;

    theorem :: WAYBEL20:10

    for L1,L2,T1,T2 be antisymmetric reflexive non empty RelStr, f be Function of L1, T1, g be Function of L2, T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds [:f, g:] is filtered-infs-preserving

    proof

      let L1,L2,T1,T2 be antisymmetric reflexive non empty RelStr, f be Function of L1, T1, g be Function of L2, T2 such that

       A1: f is filtered-infs-preserving and

       A2: g is filtered-infs-preserving;

      let X be Subset of [:L1, L2:];

      assume

       A3: X is non empty filtered;

      then ( proj1 X) is non empty filtered by YELLOW_3: 21, YELLOW_3: 24;

      then

       A4: f preserves_inf_of ( proj1 X) by A1;

      ( proj2 X) is non empty filtered by A3, YELLOW_3: 21, YELLOW_3: 24;

      then

       A5: g preserves_inf_of ( proj2 X) by A2;

      set iX = ( [:f, g:] .: X);

      

       A6: ( dom f) = the carrier of L1 & ( dom g) = the carrier of L2 by FUNCT_2:def 1;

      assume

       A7: ex_inf_of (X, [:L1, L2:]);

      then

       A8: ex_inf_of (( proj1 X),L1) by YELLOW_3: 42;

      X c= the carrier of [:L1, L2:];

      then

       A9: X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;

      then

       A10: ( proj2 iX) = (g .: ( proj2 X)) by A6, Th4;

      

       A11: ex_inf_of (( proj2 X),L2) by A7, YELLOW_3: 42;

      then

       A12: ex_inf_of (( proj2 iX),T2) by A5, A10;

      

       A13: ( proj1 iX) = (f .: ( proj1 X)) by A6, A9, Th4;

      then ex_inf_of (( proj1 iX),T1) by A4, A8;

      hence ex_inf_of (( [:f, g:] .: X), [:T1, T2:]) by A12, YELLOW_3: 42;

      

      hence ( inf ( [:f, g:] .: X)) = [( inf (f .: ( proj1 X))), ( inf (g .: ( proj2 X)))] by A13, A10, Th7

      .= [(f . ( inf ( proj1 X))), ( inf (g .: ( proj2 X)))] by A4, A8

      .= [(f . ( inf ( proj1 X))), (g . ( inf ( proj2 X)))] by A5, A11

      .= ( [:f, g:] . (( inf ( proj1 X)),( inf ( proj2 X)))) by A6, FUNCT_3:def 8

      .= ( [:f, g:] . ( inf X)) by A7, Th7;

    end;

    theorem :: WAYBEL20:11

    for L1,L2,T1,T2 be antisymmetric non empty RelStr, f be Function of L1, T1, g be Function of L2, T2 st f is sups-preserving & g is sups-preserving holds [:f, g:] is sups-preserving

    proof

      let L1,L2,T1,T2 be antisymmetric non empty RelStr, f be Function of L1, T1, g be Function of L2, T2 such that

       A1: f is sups-preserving and

       A2: g is sups-preserving;

      let X be Subset of [:L1, L2:];

      

       A3: f preserves_sup_of ( proj1 X) by A1;

      

       A4: g preserves_sup_of ( proj2 X) by A2;

      set iX = ( [:f, g:] .: X);

      

       A5: ( dom f) = the carrier of L1 & ( dom g) = the carrier of L2 by FUNCT_2:def 1;

      assume

       A6: ex_sup_of (X, [:L1, L2:]);

      then

       A7: ex_sup_of (( proj1 X),L1) by YELLOW_3: 41;

      

       A8: ex_sup_of (( proj2 X),L2) by A6, YELLOW_3: 41;

      X c= the carrier of [:L1, L2:];

      then

       A9: X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;

      then

       A10: ( proj2 iX) = (g .: ( proj2 X)) by A5, Th4;

      then

       A11: ex_sup_of (( proj2 iX),T2) by A4, A8;

      

       A12: ( proj1 iX) = (f .: ( proj1 X)) by A5, A9, Th4;

      then ex_sup_of (( proj1 iX),T1) by A3, A7;

      hence ex_sup_of (( [:f, g:] .: X), [:T1, T2:]) by A11, YELLOW_3: 41;

      

      hence ( sup ( [:f, g:] .: X)) = [( sup (f .: ( proj1 X))), ( sup (g .: ( proj2 X)))] by A12, A10, Th8

      .= [(f . ( sup ( proj1 X))), ( sup (g .: ( proj2 X)))] by A3, A7

      .= [(f . ( sup ( proj1 X))), (g . ( sup ( proj2 X)))] by A4, A8

      .= ( [:f, g:] . (( sup ( proj1 X)),( sup ( proj2 X)))) by A5, FUNCT_3:def 8

      .= ( [:f, g:] . ( sup X)) by A6, Th8;

    end;

    theorem :: WAYBEL20:12

    

     Th12: for L1,L2,T1,T2 be antisymmetric reflexive non empty RelStr, f be Function of L1, T1, g be Function of L2, T2 st f is directed-sups-preserving & g is directed-sups-preserving holds [:f, g:] is directed-sups-preserving

    proof

      let L1,L2,T1,T2 be antisymmetric reflexive non empty RelStr, f be Function of L1, T1, g be Function of L2, T2 such that

       A1: f is directed-sups-preserving and

       A2: g is directed-sups-preserving;

      let X be Subset of [:L1, L2:];

      assume

       A3: X is non empty directed;

      then ( proj1 X) is non empty directed by YELLOW_3: 21, YELLOW_3: 22;

      then

       A4: f preserves_sup_of ( proj1 X) by A1;

      ( proj2 X) is non empty directed by A3, YELLOW_3: 21, YELLOW_3: 22;

      then

       A5: g preserves_sup_of ( proj2 X) by A2;

      set iX = ( [:f, g:] .: X);

      

       A6: ( dom f) = the carrier of L1 & ( dom g) = the carrier of L2 by FUNCT_2:def 1;

      assume

       A7: ex_sup_of (X, [:L1, L2:]);

      then

       A8: ex_sup_of (( proj1 X),L1) by YELLOW_3: 41;

      X c= the carrier of [:L1, L2:];

      then

       A9: X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;

      then

       A10: ( proj2 iX) = (g .: ( proj2 X)) by A6, Th4;

      

       A11: ex_sup_of (( proj2 X),L2) by A7, YELLOW_3: 41;

      then

       A12: ex_sup_of (( proj2 iX),T2) by A5, A10;

      

       A13: ( proj1 iX) = (f .: ( proj1 X)) by A6, A9, Th4;

      then ex_sup_of (( proj1 iX),T1) by A4, A8;

      hence ex_sup_of (( [:f, g:] .: X), [:T1, T2:]) by A12, YELLOW_3: 41;

      

      hence ( sup ( [:f, g:] .: X)) = [( sup (f .: ( proj1 X))), ( sup (g .: ( proj2 X)))] by A13, A10, Th8

      .= [(f . ( sup ( proj1 X))), ( sup (g .: ( proj2 X)))] by A4, A8

      .= [(f . ( sup ( proj1 X))), (g . ( sup ( proj2 X)))] by A5, A11

      .= ( [:f, g:] . (( sup ( proj1 X)),( sup ( proj2 X)))) by A6, FUNCT_3:def 8

      .= ( [:f, g:] . ( sup X)) by A7, Th8;

    end;

    theorem :: WAYBEL20:13

    

     Th13: for L be antisymmetric non empty RelStr, X be Subset of [:L, L:] st X c= ( id the carrier of L) & ex_inf_of (X, [:L, L:]) holds ( inf X) in ( id the carrier of L)

    proof

      let L be antisymmetric non empty RelStr, X be Subset of [:L, L:];

      assume X c= ( id the carrier of L) & ex_inf_of (X, [:L, L:]);

      then ( inf X) = [( inf ( proj1 X)), ( inf ( proj2 X))] & ( inf ( proj1 X)) = ( inf ( proj2 X)) by Th1, Th7;

      hence thesis by RELAT_1:def 10;

    end;

    theorem :: WAYBEL20:14

    

     Th14: for L be antisymmetric non empty RelStr, X be Subset of [:L, L:] st X c= ( id the carrier of L) & ex_sup_of (X, [:L, L:]) holds ( sup X) in ( id the carrier of L)

    proof

      let L be antisymmetric non empty RelStr, X be Subset of [:L, L:];

      assume X c= ( id the carrier of L) & ex_sup_of (X, [:L, L:]);

      then ( sup X) = [( sup ( proj1 X)), ( sup ( proj2 X))] & ( sup ( proj1 X)) = ( sup ( proj2 X)) by Th1, Th8;

      hence thesis by RELAT_1:def 10;

    end;

    theorem :: WAYBEL20:15

    

     Th15: for L,M be non empty RelStr st (L,M) are_isomorphic & L is reflexive holds M is reflexive

    proof

      let L,M be non empty RelStr such that

       A1: (L,M) are_isomorphic and

       A2: L is reflexive;

      let x be Element of M;

      (M,L) are_isomorphic by A1, WAYBEL_1: 6;

      then

      consider f be Function of M, L such that

       A3: f is isomorphic;

      reconsider fx = (f . x) as Element of L;

      fx <= fx by A2;

      hence thesis by A3, WAYBEL_0: 66;

    end;

    theorem :: WAYBEL20:16

    

     Th16: for L,M be non empty RelStr st (L,M) are_isomorphic & L is transitive holds M is transitive

    proof

      let L,M be non empty RelStr such that

       A1: (L,M) are_isomorphic and

       A2: L is transitive;

      (M,L) are_isomorphic by A1, WAYBEL_1: 6;

      then

      consider f be Function of M, L such that

       A3: f is isomorphic;

      let x,y,z be Element of M such that

       A4: x <= y & y <= z;

      reconsider fz = (f . z) as Element of L;

      reconsider fy = (f . y) as Element of L;

      reconsider fx = (f . x) as Element of L;

      fx <= fy & fy <= fz by A3, A4, WAYBEL_0: 66;

      then fx <= fz by A2;

      hence thesis by A3, WAYBEL_0: 66;

    end;

    theorem :: WAYBEL20:17

    

     Th17: for L,M be non empty RelStr st (L,M) are_isomorphic & L is antisymmetric holds M is antisymmetric

    proof

      let L,M be non empty RelStr such that

       A1: (L,M) are_isomorphic and

       A2: L is antisymmetric;

      (M,L) are_isomorphic by A1, WAYBEL_1: 6;

      then

      consider f be Function of M, L such that

       A3: f is isomorphic;

      let x,y be Element of M such that

       A4: x <= y & y <= x;

      reconsider fy = (f . y) as Element of L;

      reconsider fx = (f . x) as Element of L;

      fx <= fy & fy <= fx by A3, A4, WAYBEL_0: 66;

      then ( dom f) = the carrier of M & fx = fy by A2, FUNCT_2:def 1;

      hence thesis by A3, FUNCT_1:def 4;

    end;

    theorem :: WAYBEL20:18

    

     Th18: for L,M be non empty RelStr st (L,M) are_isomorphic & L is complete holds M is complete

    proof

      let L,M be non empty RelStr such that

       A1: (L,M) are_isomorphic and

       A2: L is complete;

      let X be Subset of M;

      (M,L) are_isomorphic by A1, WAYBEL_1: 6;

      then

      consider f be Function of M, L such that

       A3: f is isomorphic;

      reconsider fX = (f .: X) as Subset of L;

      consider fa be Element of L such that

       A4: fa is_<=_than fX and

       A5: for fb be Element of L st fb is_<=_than fX holds fb <= fa by A2;

      set a = ((f qua Function " ) . fa);

      

       A6: ( rng f) = the carrier of L by A3, WAYBEL_0: 66;

      then a in ( dom f) by A3, FUNCT_1: 32;

      then

      reconsider a as Element of M;

      

       A7: fa = (f . a) by A3, A6, FUNCT_1: 35;

      take a;

      

       A8: ( dom f) = the carrier of M by FUNCT_2:def 1;

      hereby

        let b be Element of M such that

         A9: b in X;

        reconsider fb = (f . b) as Element of L;

        fb in fX by A8, A9, FUNCT_1:def 6;

        then fa <= fb by A4;

        hence a <= b by A3, A7, WAYBEL_0: 66;

      end;

      let b be Element of M such that

       A10: b is_<=_than X;

      reconsider fb = (f . b) as Element of L;

      fb is_<=_than fX

      proof

        let fc be Element of L;

        assume fc in fX;

        then

        consider c be object such that

         A11: c in ( dom f) and

         A12: c in X and

         A13: fc = (f . c) by FUNCT_1:def 6;

        reconsider c as Element of M by A11;

        b <= c by A10, A12;

        hence thesis by A3, A13, WAYBEL_0: 66;

      end;

      then fb <= fa by A5;

      hence thesis by A3, A7, WAYBEL_0: 66;

    end;

    theorem :: WAYBEL20:19

    

     Th19: for L be non empty transitive RelStr, k be Function of L, L st k is infs-preserving holds ( corestr k) is infs-preserving

    proof

      let L be non empty transitive RelStr, k be Function of L, L such that

       A1: k is infs-preserving;

      let X be Subset of L;

      assume

       A2: ex_inf_of (X,L);

      set f = ( corestr k);

      

       A3: k = ( corestr k) by WAYBEL_1: 30;

      

       A4: k preserves_inf_of X by A1;

      then

       A5: ex_inf_of ((k .: X),L) by A2;

      reconsider fX = (f .: X) as Subset of ( Image k);

      ( dom k) = the carrier of L by FUNCT_2:def 1;

      then ( rng k) = the carrier of ( Image k) & (k . ( inf X)) in ( rng k) by FUNCT_1:def 3, YELLOW_0:def 15;

      then ( "/\" (fX,L)) is Element of ( Image k) by A4, A3, A2;

      hence ex_inf_of ((f .: X),( Image k)) by A3, A5, YELLOW_0: 63;

      ( inf (k .: X)) = (k . ( inf X)) by A4, A2;

      hence thesis by A3, A5, YELLOW_0: 63;

    end;

    theorem :: WAYBEL20:20

    for L be non empty transitive RelStr, k be Function of L, L st k is filtered-infs-preserving holds ( corestr k) is filtered-infs-preserving

    proof

      let L be non empty transitive RelStr, k be Function of L, L such that

       A1: k is filtered-infs-preserving;

      let X be Subset of L;

      assume X is non empty filtered;

      then

       A2: k preserves_inf_of X by A1;

      set f = ( corestr k);

      

       A3: k = ( corestr k) by WAYBEL_1: 30;

      assume

       A4: ex_inf_of (X,L);

      then

       A5: ex_inf_of ((k .: X),L) by A2;

      reconsider fX = (f .: X) as Subset of ( Image k);

      ( dom k) = the carrier of L by FUNCT_2:def 1;

      then ( rng k) = the carrier of ( Image k) & (k . ( inf X)) in ( rng k) by FUNCT_1:def 3, YELLOW_0:def 15;

      then ( "/\" (fX,L)) is Element of ( Image k) by A2, A3, A4;

      hence ex_inf_of ((f .: X),( Image k)) by A3, A5, YELLOW_0: 63;

      ( inf (k .: X)) = (k . ( inf X)) by A2, A4;

      hence thesis by A3, A5, YELLOW_0: 63;

    end;

    theorem :: WAYBEL20:21

    for L be non empty transitive RelStr, k be Function of L, L st k is sups-preserving holds ( corestr k) is sups-preserving

    proof

      let L be non empty transitive RelStr, k be Function of L, L such that

       A1: k is sups-preserving;

      let X be Subset of L;

      assume

       A2: ex_sup_of (X,L);

      set f = ( corestr k);

      

       A3: k = ( corestr k) by WAYBEL_1: 30;

      

       A4: k preserves_sup_of X by A1;

      then

       A5: ex_sup_of ((k .: X),L) by A2;

      reconsider fX = (f .: X) as Subset of ( Image k);

      ( dom k) = the carrier of L by FUNCT_2:def 1;

      then ( rng k) = the carrier of ( Image k) & (k . ( sup X)) in ( rng k) by FUNCT_1:def 3, YELLOW_0:def 15;

      then ( "\/" (fX,L)) is Element of ( Image k) by A4, A3, A2;

      hence ex_sup_of ((f .: X),( Image k)) by A3, A5, YELLOW_0: 64;

      ( sup (k .: X)) = (k . ( sup X)) by A4, A2;

      hence thesis by A3, A5, YELLOW_0: 64;

    end;

    theorem :: WAYBEL20:22

    

     Th22: for L be non empty transitive RelStr, k be Function of L, L st k is directed-sups-preserving holds ( corestr k) is directed-sups-preserving

    proof

      let L be non empty transitive RelStr, k be Function of L, L such that

       A1: k is directed-sups-preserving;

      let X be Subset of L;

      assume X is non empty directed;

      then

       A2: k preserves_sup_of X by A1;

      set f = ( corestr k);

      

       A3: k = ( corestr k) by WAYBEL_1: 30;

      assume

       A4: ex_sup_of (X,L);

      then

       A5: ex_sup_of ((k .: X),L) by A2;

      reconsider fX = (f .: X) as Subset of ( Image k);

      ( dom k) = the carrier of L by FUNCT_2:def 1;

      then ( rng k) = the carrier of ( Image k) & (k . ( sup X)) in ( rng k) by FUNCT_1:def 3, YELLOW_0:def 15;

      then ( "\/" (fX,L)) is Element of ( Image k) by A2, A3, A4;

      hence ex_sup_of ((f .: X),( Image k)) by A3, A5, YELLOW_0: 64;

      ( sup (k .: X)) = (k . ( sup X)) by A2, A4;

      hence thesis by A3, A5, YELLOW_0: 64;

    end;

    theorem :: WAYBEL20:23

    

     Th23: for S,T be reflexive antisymmetric non empty RelStr, f be Function of S, T st f is filtered-infs-preserving holds f is monotone

    proof

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

      assume

       A1: f is filtered-infs-preserving;

      let x,y be Element of S such that

       A2: x <= y;

      

       A3: ( dom f) = the carrier of S by FUNCT_2:def 1;

      

       A4: for b be Element of S st {x, y} is_>=_than b holds x >= b by YELLOW_0: 8;

      

       A5: x <= x;

      then

       A6: {x, y} is_>=_than x by A2, YELLOW_0: 8;

      then

       A7: ex_inf_of ( {x, y},S) by A4, YELLOW_0: 31;

      for a,b be Element of S st a in {x, y} & b in {x, y} holds ex z be Element of S st z in {x, y} & a >= z & b >= z

      proof

        let a,b be Element of S such that

         A8: a in {x, y} & b in {x, y};

        take x;

        thus x in {x, y} by TARSKI:def 2;

        thus thesis by A2, A5, A8, TARSKI:def 2;

      end;

      then {x, y} is filtered non empty;

      then

       A9: f preserves_inf_of {x, y} by A1;

      x = ( inf {x, y}) by A6, A4, YELLOW_0: 31;

      then ( inf (f .: {x, y})) = (f . x) by A7, A9;

      then

       A10: (f . x) = ( inf {(f . x), (f . y)}) by A3, FUNCT_1: 60;

      (f .: {x, y}) = {(f . x), (f . y)} by A3, FUNCT_1: 60;

      then ex_inf_of ( {(f . x), (f . y)},T) by A7, A9;

      then {(f . x), (f . y)} is_>=_than (f . x) by A10, YELLOW_0:def 10;

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

    end;

    theorem :: WAYBEL20:24

    

     Th24: for S,T be non empty RelStr, f be Function of S, T st f is monotone holds for X be Subset of S holds (X is filtered implies (f .: X) is filtered)

    proof

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

      assume

       A1: f is monotone;

      let X be Subset of S such that

       A2: X is filtered;

      let x,y be Element of T;

      assume x in (f .: X);

      then

      consider a be object such that

       A3: a in the carrier of S and

       A4: a in X and

       A5: x = (f . a) by FUNCT_2: 64;

      assume y in (f .: X);

      then

      consider b be object such that

       A6: b in the carrier of S and

       A7: b in X and

       A8: y = (f . b) by FUNCT_2: 64;

      reconsider a, b as Element of S by A3, A6;

      consider c be Element of S such that

       A9: c in X and

       A10: c <= a & c <= b by A2, A4, A7;

      take z = (f . c);

      thus z in (f .: X) by A9, FUNCT_2: 35;

      thus thesis by A1, A5, A8, A10;

    end;

    theorem :: WAYBEL20:25

    

     Th25: for L1,L2,L3 be non empty RelStr, f be Function of L1, L2, g be Function of L2, L3 st f is infs-preserving & g is infs-preserving holds (g * f) is infs-preserving

    proof

      let L1,L2,L3 be non empty RelStr, f be Function of L1, L2, g be Function of L2, L3 such that

       A1: f is infs-preserving and

       A2: g is infs-preserving;

      set gf = (g * f);

      let X be Subset of L1 such that

       A3: ex_inf_of (X,L1);

      set fX = (f .: X);

      set gfX = (gf .: X);

      

       A4: f preserves_inf_of X by A1;

      then

       A5: gfX = (g .: (f .: X)) & ex_inf_of (fX,L2) by A3, RELAT_1: 126;

      

       A6: ( dom f) = the carrier of L1 by FUNCT_2:def 1;

      

       A7: g preserves_inf_of fX by A2;

      hence ex_inf_of (gfX,L3) by A5;

      

      thus ( inf gfX) = (g . ( inf fX)) by A7, A5

      .= (g . (f . ( inf X))) by A3, A4

      .= (gf . ( inf X)) by A6, FUNCT_1: 13;

    end;

    theorem :: WAYBEL20:26

    for L1,L2,L3 be non empty reflexive antisymmetric RelStr, f be Function of L1, L2, g be Function of L2, L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds (g * f) is filtered-infs-preserving

    proof

      let L1,L2,L3 be non empty reflexive antisymmetric RelStr, f be Function of L1, L2, g be Function of L2, L3 such that

       A1: f is filtered-infs-preserving and

       A2: g is filtered-infs-preserving;

      set gf = (g * f);

      let X be Subset of L1 such that

       A3: X is non empty filtered and

       A4: ex_inf_of (X,L1);

      set xx = the Element of X;

      set fX = (f .: X);

      set gfX = (gf .: X);

      

       A5: f preserves_inf_of X by A1, A3;

      then

       A6: gfX = (g .: (f .: X)) & ex_inf_of (fX,L2) by A4, RELAT_1: 126;

      xx in X by A3;

      then (f . xx) in fX by FUNCT_2: 35;

      then fX is non empty filtered by A1, A3, Th23, Th24;

      then

       A7: g preserves_inf_of fX by A2;

      hence ex_inf_of (gfX,L3) by A6;

      

       A8: ( dom f) = the carrier of L1 by FUNCT_2:def 1;

      

      thus ( inf gfX) = (g . ( inf fX)) by A7, A6

      .= (g . (f . ( inf X))) by A4, A5

      .= (gf . ( inf X)) by A8, FUNCT_1: 13;

    end;

    theorem :: WAYBEL20:27

    for L1,L2,L3 be non empty RelStr, f be Function of L1, L2, g be Function of L2, L3 st f is sups-preserving & g is sups-preserving holds (g * f) is sups-preserving

    proof

      let L1,L2,L3 be non empty RelStr, f be Function of L1, L2, g be Function of L2, L3 such that

       A1: f is sups-preserving and

       A2: g is sups-preserving;

      set gf = (g * f);

      let X be Subset of L1 such that

       A3: ex_sup_of (X,L1);

      set fX = (f .: X);

      set gfX = (gf .: X);

      

       A4: f preserves_sup_of X by A1;

      then

       A5: gfX = (g .: (f .: X)) & ex_sup_of (fX,L2) by A3, RELAT_1: 126;

      

       A6: ( dom f) = the carrier of L1 by FUNCT_2:def 1;

      

       A7: g preserves_sup_of fX by A2;

      hence ex_sup_of (gfX,L3) by A5;

      

      thus ( sup gfX) = (g . ( sup fX)) by A7, A5

      .= (g . (f . ( sup X))) by A3, A4

      .= (gf . ( sup X)) by A6, FUNCT_1: 13;

    end;

    theorem :: WAYBEL20:28

    for L1,L2,L3 be non empty reflexive antisymmetric RelStr, f be Function of L1, L2, g be Function of L2, L3 st f is directed-sups-preserving & g is directed-sups-preserving holds (g * f) is directed-sups-preserving

    proof

      let L1,L2,L3 be non empty reflexive antisymmetric RelStr, f be Function of L1, L2, g be Function of L2, L3 such that

       A1: f is directed-sups-preserving and

       A2: g is directed-sups-preserving;

      set gf = (g * f);

      let X be Subset of L1 such that

       A3: X is non empty directed and

       A4: ex_sup_of (X,L1);

      set xx = the Element of X;

      set fX = (f .: X);

      set gfX = (gf .: X);

      

       A5: f preserves_sup_of X by A1, A3;

      then

       A6: gfX = (g .: (f .: X)) & ex_sup_of (fX,L2) by A4, RELAT_1: 126;

      xx in X by A3;

      then (f . xx) in fX by FUNCT_2: 35;

      then fX is non empty directed by A1, A3, WAYBEL17: 3, YELLOW_2: 15;

      then

       A7: g preserves_sup_of fX by A2;

      hence ex_sup_of (gfX,L3) by A6;

      

       A8: ( dom f) = the carrier of L1 by FUNCT_2:def 1;

      

      thus ( sup gfX) = (g . ( sup fX)) by A7, A6

      .= (g . (f . ( sup X))) by A4, A5

      .= (gf . ( sup X)) by A8, FUNCT_1: 13;

    end;

    begin

    theorem :: WAYBEL20:29

    for I be non empty set holds for J be RelStr-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is lower-bounded antisymmetric RelStr holds ( product J) is lower-bounded

    proof

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

       A1: for i be Element of I holds (J . i) is lower-bounded antisymmetric RelStr;

      deffunc F( Element of I) = ( Bottom (J . $1));

      consider f be ManySortedSet of I such that

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

       A3:

      now

        let i be Element of I;

        (f . i) = ( Bottom (J . i)) by A2;

        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 A3, WAYBEL_3: 27;

      take f;

      let b be Element of ( product J) such that b in the carrier of ( product J);

      now

        let i be Element of I;

        (f . i) = ( Bottom (J . i)) & (J . i) is lower-bounded antisymmetric non empty RelStr by A1, A2;

        hence (f . i) <= (b . i) by YELLOW_0: 44;

      end;

      hence thesis by WAYBEL_3: 28;

    end;

    theorem :: WAYBEL20:30

    for I be non empty set holds for J be RelStr-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is upper-bounded antisymmetric RelStr holds ( product J) is upper-bounded

    proof

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

       A1: for i be Element of I holds (J . i) is upper-bounded antisymmetric RelStr;

      deffunc F( Element of I) = ( Top (J . $1));

      consider f be ManySortedSet of I such that

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

       A3:

      now

        let i be Element of I;

        (f . i) = ( Top (J . i)) by A2;

        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 A3, WAYBEL_3: 27;

      take f;

      let b be Element of ( product J) such that b in the carrier of ( product J);

      now

        let i be Element of I;

        (f . i) = ( Top (J . i)) & (J . i) is upper-bounded antisymmetric non empty RelStr by A1, A2;

        hence (f . i) >= (b . i) by YELLOW_0: 45;

      end;

      hence thesis by WAYBEL_3: 28;

    end;

    theorem :: WAYBEL20:31

    for I be non empty set holds for J be RelStr-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is lower-bounded antisymmetric RelStr holds for i be Element of I holds (( Bottom ( product J)) . i) = ( Bottom (J . i))

    proof

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

       A1: for i be Element of I holds (J . i) is lower-bounded antisymmetric RelStr;

      deffunc F( Element of I) = ( Bottom (J . $1));

      consider f be ManySortedSet of I such that

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

       A3:

      now

        let i be Element of I;

        (f . i) = ( Bottom (J . i)) by A2;

        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 A3, WAYBEL_3: 27;

      let i be Element of I;

      

       A4: {} is_<=_than f;

       A5:

      now

        let c be Element of ( product J) such that {} is_<=_than c and

         A6: for b be Element of ( product J) st {} is_<=_than b holds b >= c;

        now

          let i be Element of I;

          (f . i) = ( Bottom (J . i)) & (J . i) is lower-bounded antisymmetric non empty RelStr by A1, A2;

          hence (f . i) <= (c . i) by YELLOW_0: 44;

        end;

        then

         A7: f <= c by WAYBEL_3: 28;

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

        then

         A8: ( product J) is antisymmetric by WAYBEL_3: 30;

        c <= f by A6, YELLOW_0: 6;

        hence c = f by A8, A7;

      end;

       A9:

      now

        let a be Element of ( product J) such that {} is_<=_than a;

        now

          let i be Element of I;

          (f . i) = ( Bottom (J . i)) & (J . i) is lower-bounded antisymmetric non empty RelStr by A1, A2;

          hence (f . i) <= (a . i) by YELLOW_0: 44;

        end;

        hence f <= a by WAYBEL_3: 28;

      end;

      now

        let b be Element of ( product J) such that {} is_<=_than b;

        now

          let i be Element of I;

          (f . i) = ( Bottom (J . i)) & (J . i) is lower-bounded antisymmetric non empty RelStr by A1, A2;

          hence (f . i) <= (b . i) by YELLOW_0: 44;

        end;

        hence f <= b by WAYBEL_3: 28;

      end;

      then ex_sup_of ( {} ,( product J)) by A4, A5;

      then f = ( "\/" ( {} ,( product J))) by A4, A9, YELLOW_0:def 9;

      hence thesis by A2;

    end;

    theorem :: WAYBEL20:32

    for I be non empty set holds for J be RelStr-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is upper-bounded antisymmetric RelStr holds for i be Element of I holds (( Top ( product J)) . i) = ( Top (J . i))

    proof

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

       A1: for i be Element of I holds (J . i) is upper-bounded antisymmetric RelStr;

      deffunc F( Element of I) = ( Top (J . $1));

      consider f be ManySortedSet of I such that

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

       A3:

      now

        let i be Element of I;

        (f . i) = ( Top (J . i)) by A2;

        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 A3, WAYBEL_3: 27;

      let i be Element of I;

      

       A4: {} is_>=_than f;

       A5:

      now

        let c be Element of ( product J) such that {} is_>=_than c and

         A6: for b be Element of ( product J) st {} is_>=_than b holds b <= c;

        now

          let i be Element of I;

          (f . i) = ( Top (J . i)) & (J . i) is upper-bounded antisymmetric non empty RelStr by A1, A2;

          hence (f . i) >= (c . i) by YELLOW_0: 45;

        end;

        then

         A7: f >= c by WAYBEL_3: 28;

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

        then

         A8: ( product J) is antisymmetric by WAYBEL_3: 30;

        c >= f by A6, YELLOW_0: 6;

        hence c = f by A8, A7;

      end;

       A9:

      now

        let a be Element of ( product J) such that {} is_>=_than a;

        now

          let i be Element of I;

          (f . i) = ( Top (J . i)) & (J . i) is upper-bounded antisymmetric non empty RelStr by A1, A2;

          hence (f . i) >= (a . i) by YELLOW_0: 45;

        end;

        hence f >= a by WAYBEL_3: 28;

      end;

      now

        let b be Element of ( product J) such that {} is_>=_than b;

        now

          let i be Element of I;

          (f . i) = ( Top (J . i)) & (J . i) is upper-bounded antisymmetric non empty RelStr by A1, A2;

          hence (f . i) >= (b . i) by YELLOW_0: 45;

        end;

        hence f >= b by WAYBEL_3: 28;

      end;

      then ex_inf_of ( {} ,( product J)) by A4, A5;

      then f = ( "/\" ( {} ,( product J))) by A4, A9, YELLOW_0:def 10;

      hence thesis by A2;

    end;

    theorem :: WAYBEL20:33

    for I be non empty set, J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is continuous complete LATTICE holds ( product J) is continuous

    proof

      let I be non empty set, J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is continuous complete LATTICE;

      

       A2: for i be Element of I holds (J . i) is complete LATTICE by A1;

      set pJ = ( product J);

      reconsider pJ9 = pJ as complete LATTICE by A2, WAYBEL_3: 31;

      hereby

        let x be Element of pJ;

        reconsider x9 = x as Element of pJ9;

        ( waybelow x9) is non empty;

        hence ( waybelow x) is non empty;

        ( waybelow x9) is directed;

        hence ( waybelow x) is directed;

      end;

      pJ9 is up-complete;

      hence pJ is up-complete;

      let x be Element of pJ;

      set swx = ( sup ( waybelow x));

      now

        thus ( dom x) = I by WAYBEL_3: 27;

        thus ( dom swx) = I by WAYBEL_3: 27;

        let i be object;

        assume i in I;

        then

        reconsider i9 = i as Element of I;

        now

          reconsider K = {i9} as finite Subset of I;

          deffunc F( Element of I) = ( Bottom (J . $1));

          let a be object;

          consider g be ManySortedSet of I such that

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

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

          hereby

            assume a in ( pi (( waybelow x),i9));

            then

            consider f be Function such that

             A4: f in ( waybelow x) and

             A5: a = (f . i) by CARD_3:def 6;

            reconsider f as Element of pJ by A4;

            f << x by A4, WAYBEL_3: 7;

            then (f . i9) << (x . i9) by A2, WAYBEL_3: 33;

            hence a in ( waybelow (x . i9)) by A5;

          end;

          

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

          then

           A7: ( dom f) = I by FUNCT_7: 30;

          assume

           A8: a in ( waybelow (x . i9));

          now

            let j be Element of I;

            per cases ;

              suppose i9 = j;

              hence (f . j) is Element of (J . j) by A8, A6, FUNCT_7: 31;

            end;

              suppose i9 <> j;

              

              then (f . j) = (g . j) by FUNCT_7: 32

              .= ( Bottom (J . j)) by A3;

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

            end;

          end;

          then

          reconsider f as Element of pJ by A7, WAYBEL_3: 27;

           A9:

          now

            let j be Element of I;

            per cases ;

              suppose

               A10: i9 = j;

              (f . i9) = a by A6, FUNCT_7: 31;

              hence (f . j) << (x . j) by A8, A10, WAYBEL_3: 7;

            end;

              suppose

               A11: i9 <> j;

              

               A12: (J . j) is complete LATTICE by A1;

              (f . j) = (g . j) by A11, FUNCT_7: 32

              .= ( Bottom (J . j)) by A3;

              hence (f . j) << (x . j) by A12, WAYBEL_3: 4;

            end;

          end;

          now

            let j be Element of I;

            assume not j in K;

            then j <> i9 by TARSKI:def 1;

            

            hence (f . j) = (g . j) by FUNCT_7: 32

            .= ( Bottom (J . j)) by A3;

          end;

          then f << x by A2, A9, WAYBEL_3: 33;

          then

           A13: f in ( waybelow x);

          a = (f . i9) by A6, FUNCT_7: 31;

          hence a in ( pi (( waybelow x),i9)) by A13, CARD_3:def 6;

        end;

        then

         A14: ( pi (( waybelow x),i9)) = ( waybelow (x . i9)) by TARSKI: 2;

        (swx . i9) = ( sup ( pi (( waybelow x),i9))) & (J . i9) is satisfying_axiom_of_approximation by A1, A2, WAYBEL_3: 32;

        hence (x . i) = (swx . i) by A14;

      end;

      hence thesis by FUNCT_1: 2;

    end;

    begin

    theorem :: WAYBEL20:34

    

     Th34: for L,T be continuous complete LATTICE, g be CLHomomorphism of L, T, S be Subset of [:L, L:] st S = ( [:g, g:] " ( id the carrier of T)) holds ( subrelstr S) is CLSubFrame of [:L, L:]

    proof

      let L,T be continuous complete LATTICE, g be CLHomomorphism of L, T, SL be Subset of [:L, L:] such that

       A1: SL = ( [:g, g:] " ( id the carrier of T));

      set x = the Element of L;

      

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

      then

       A3: [x, x] in [:( dom g), ( dom g):] by ZFMISC_1: 87;

       [(g . x), (g . x)] in ( id the carrier of T) by RELAT_1:def 10;

      then ( dom [:g, g:]) = [:( dom g), ( dom g):] & ( [:g, g:] . (x,x)) in ( id the carrier of T) by A2, FUNCT_3:def 8;

      then

      reconsider nSL = SL as non empty Subset of [:L, L:] by A1, A3, FUNCT_1:def 7;

      set pL = [:L, L:], pg = [:g, g:];

      

       A4: g is infs-preserving directed-sups-preserving by WAYBEL16:def 1;

      

       A5: the carrier of pL = [:the carrier of L, the carrier of L:] by YELLOW_3:def 2;

      

       A6: ( subrelstr nSL) is non empty;

      

       A7: ( subrelstr SL) is directed-sups-inheriting

      proof

        let X be directed Subset of ( subrelstr SL) such that

         A8: X <> {} and

         A9: ex_sup_of (X,pL);

        reconsider X9 = X as directed non empty Subset of pL by A6, A8, YELLOW_2: 7;

        pg is directed-sups-preserving by A4, Th12;

        then pg preserves_sup_of X9;

        then

         A10: ( sup (pg .: X9)) = (pg . ( sup X9)) by A9;

        X c= the carrier of ( subrelstr SL);

        then X c= SL by YELLOW_0:def 15;

        then

         A11: (pg .: X) c= (pg .: SL) by RELAT_1: 123;

        (pg .: SL) c= ( id the carrier of T) & ex_sup_of ((pg .: X9), [:T, T:]) by A1, FUNCT_1: 75, YELLOW_0: 17;

        then

         A12: ( sup (pg .: X9)) in ( id the carrier of T) by A11, Th14, XBOOLE_1: 1;

        consider x,y be object such that

         A13: x in the carrier of L & y in the carrier of L and

         A14: ( sup X9) = [x, y] by A5, ZFMISC_1:def 2;

         [x, y] in [:( dom g), ( dom g):] by A2, A13, ZFMISC_1: 87;

        then [x, y] in ( dom [:g, g:]) by FUNCT_3:def 8;

        then [x, y] in ( [:g, g:] " ( id the carrier of T)) by A14, A10, A12, FUNCT_1:def 7;

        hence thesis by A1, A14, YELLOW_0:def 15;

      end;

      ( subrelstr SL) is infs-inheriting

      proof

        let X be Subset of ( subrelstr SL) such that

         A15: ex_inf_of (X,pL);

        X c= the carrier of ( subrelstr SL);

        then

         A16: X c= SL by YELLOW_0:def 15;

        then

        reconsider X9 = X as Subset of pL by XBOOLE_1: 1;

        

         A17: (pg .: SL) c= ( id the carrier of T) & ex_inf_of ((pg .: X9), [:T, T:]) by A1, FUNCT_1: 75, YELLOW_0: 17;

        pg is infs-preserving by A4, Th9;

        then pg preserves_inf_of X9;

        then

         A18: ( inf (pg .: X9)) = (pg . ( inf X9)) by A15;

        (pg .: X) c= (pg .: SL) by A16, RELAT_1: 123;

        then

         A19: ( inf (pg .: X9)) in ( id the carrier of T) by A17, Th13, XBOOLE_1: 1;

        consider x,y be object such that

         A20: x in the carrier of L & y in the carrier of L and

         A21: ( inf X9) = [x, y] by A5, ZFMISC_1:def 2;

         [x, y] in [:( dom g), ( dom g):] by A2, A20, ZFMISC_1: 87;

        then [x, y] in ( dom [:g, g:]) by FUNCT_3:def 8;

        then [x, y] in ( [:g, g:] " ( id the carrier of T)) by A21, A18, A19, FUNCT_1:def 7;

        hence thesis by A1, A21, YELLOW_0:def 15;

      end;

      hence thesis by A7;

    end;

    definition

      let L be RelStr, R be Subset of [:L, L:];

      :: WAYBEL20:def1

      func EqRel R -> Equivalence_Relation of the carrier of L equals

      : Def1: R;

      correctness by A1;

    end

    definition

      let L be non empty RelStr, R be Subset of [:L, L:];

      :: WAYBEL20:def2

      attr R is CLCongruence means R is Equivalence_Relation of the carrier of L & ( subrelstr R) is CLSubFrame of [:L, L:];

    end

    theorem :: WAYBEL20:35

    

     Th35: for L be complete LATTICE, R be non empty Subset of [:L, L:] st R is CLCongruence holds for x be Element of L holds [( inf ( Class (( EqRel R),x))), x] in R

    proof

      let L be complete LATTICE, R be non empty Subset of [:L, L:];

      assume

       A1: R is CLCongruence;

      let x be Element of L;

      set CRx = ( Class (( EqRel R),x));

      reconsider SR = [:CRx, {x}:] as Subset of [:L, L:];

      R is Equivalence_Relation of the carrier of L by A1;

      then

       A2: R = ( EqRel R) by Def1;

      SR c= the carrier of ( subrelstr R)

      proof

        let a be object;

        assume a in SR;

        then

        consider a1,a2 be object such that

         A3: a1 in CRx and

         A4: a2 in {x} and

         A5: a = [a1, a2] by ZFMISC_1:def 2;

        a2 = x by A4, TARSKI:def 1;

        then a in R by A2, A3, A5, EQREL_1: 19;

        hence thesis by YELLOW_0:def 15;

      end;

      then

      reconsider SR9 = SR as Subset of ( subrelstr R);

      

       A6: ex_inf_of (SR, [:L, L:]) by YELLOW_0: 17;

      ( subrelstr R) is CLSubFrame of [:L, L:] by A1;

      then

       A7: ( "/\" (SR9, [:L, L:])) in the carrier of ( subrelstr R) by A6, YELLOW_0:def 18;

      

       A8: x in CRx by EQREL_1: 20;

      ( inf SR) = [( inf ( proj1 SR)), ( inf ( proj2 SR))] by Th7, YELLOW_0: 17

      .= [( inf CRx), ( inf ( proj2 SR))] by FUNCT_5: 9

      .= [( inf CRx), ( inf {x})] by A8, FUNCT_5: 9

      .= [( inf CRx), x] by YELLOW_0: 39;

      hence thesis by A7, YELLOW_0:def 15;

    end;

    definition

      let L be complete LATTICE, R be non empty Subset of [:L, L:];

      :: WAYBEL20:def3

      func kernel_op R -> kernel Function of L, L means

      : Def3: for x be Element of L holds (it . x) = ( inf ( Class (( EqRel R),x)));

      existence

      proof

        deffunc F( Element of L) = ( inf ( Class (( EqRel R),$1)));

        consider k be Function of the carrier of L, the carrier of L such that

         A2: for x be Element of L holds (k . x) = F(x) from FUNCT_2:sch 4;

        reconsider k as Function of L, L;

        R is Equivalence_Relation of the carrier of L by A1;

        then

         A3: R = ( EqRel R) by Def1;

        

         A4: ( subrelstr R) is CLSubFrame of [:L, L:] by A1;

        

         A5: k is monotone

        proof

          let x,y be Element of L such that

           A6: x <= y;

          set CRy = ( Class (( EqRel R),y));

          set CRx = ( Class (( EqRel R),x));

          reconsider SR = { [( inf CRx), x], [( inf CRy), y]} as Subset of [:L, L:];

          

           A7: ( inf SR) = [( inf ( proj1 SR)), ( inf ( proj2 SR))] by Th7, YELLOW_0: 17

          .= [( inf {( inf CRx), ( inf CRy)}), ( inf ( proj2 SR))] by FUNCT_5: 13

          .= [( inf {( inf CRx), ( inf CRy)}), ( inf {x, y})] by FUNCT_5: 13;

           [( inf CRx), x] in R & [( inf CRy), y] in R by A1, Th35;

          then SR c= R by ZFMISC_1: 32;

          then

          reconsider SR9 = SR as Subset of ( subrelstr R) by YELLOW_0:def 15;

           ex_inf_of (SR, [:L, L:]) by YELLOW_0: 17;

          then

           A8: ( "/\" (SR9, [:L, L:])) in the carrier of ( subrelstr R) by A4, YELLOW_0:def 18;

          ( inf {x, y}) = (x "/\" y) by YELLOW_0: 40

          .= x by A6, YELLOW_0: 25;

          then [( inf {( inf CRx), ( inf CRy)}), x] in R by A7, A8, YELLOW_0:def 15;

          then ( inf {( inf CRx), ( inf CRy)}) in CRx by A3, EQREL_1: 19;

          then

           A9: ( inf CRx) <= ( inf {( inf CRx), ( inf CRy)}) by YELLOW_2: 22;

          ( inf CRy) in {( inf CRx), ( inf CRy)} by TARSKI:def 2;

          then

           A10: ( inf {( inf CRx), ( inf CRy)}) <= ( inf CRy) by YELLOW_2: 22;

          (k . x) = ( inf CRx) & (k . y) = ( inf CRy) by A2;

          hence (k . x) <= (k . y) by A9, A10, YELLOW_0:def 2;

        end;

        now

          let x be Element of L;

          set CRx = ( Class (( EqRel R),x));

           [( inf CRx), x] in R by A1, Th35;

          then ( inf CRx) in CRx by A3, EQREL_1: 19;

          then

           A11: ( Class (( EqRel R),( inf CRx))) = CRx by EQREL_1: 23;

          

           A12: (k . x) = ( inf CRx) by A2;

          then (k . (k . x)) = ( inf ( Class (( EqRel R),( inf CRx)))) by A2;

          hence ((k * k) . x) = (k . x) by A12, A11, FUNCT_2: 15;

        end;

        then (k * k) = k by FUNCT_2: 63;

        then k is idempotent by QUANTAL1:def 9;

        then

         A13: k is projection by A5;

        now

          let x be Element of L;

          set CRx = ( Class (( EqRel R),x));

          x in CRx & ( inf CRx) is_<=_than CRx by EQREL_1: 20, YELLOW_0: 33;

          then

           A14: ( inf CRx) <= x;

          (k . x) = ( inf ( Class (( EqRel R),x))) by A2;

          hence (k . x) <= (( id L) . x) by A14, FUNCT_1: 18;

        end;

        then k <= ( id L) by YELLOW_2: 9;

        then

        reconsider k as kernel Function of L, L by A13, WAYBEL_1:def 15;

        take k;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let it1,it2 be kernel Function of L, L such that

         A15: for x be Element of L holds (it1 . x) = ( inf ( Class (( EqRel R),x))) and

         A16: for x be Element of L holds (it2 . x) = ( inf ( Class (( EqRel R),x)));

        now

          let x be object;

          assume x in the carrier of L;

          then

          reconsider x9 = x as Element of L;

          

          thus (it1 . x) = ( inf ( Class (( EqRel R),x9))) by A15

          .= (it2 . x) by A16;

        end;

        hence it1 = it2 by FUNCT_2: 12;

      end;

    end

    theorem :: WAYBEL20:36

    

     Th36: for L be complete LATTICE, R be non empty Subset of [:L, L:] st R is CLCongruence holds ( kernel_op R) is directed-sups-preserving & R = ( [:( kernel_op R), ( kernel_op R):] " ( id the carrier of L))

    proof

      let L be complete LATTICE, R be non empty Subset of [:L, L:];

      set k = ( kernel_op R);

      set cL = the carrier of L;

      

       A1: ( dom k) = cL by FUNCT_2:def 1;

      assume

       A2: R is CLCongruence;

      then

       A3: R is Equivalence_Relation of the carrier of L;

      then

       A4: ( EqRel R) = R by Def1;

      

       A5: ( subrelstr R) is CLSubFrame of [:L, L:] by A2;

      thus k is directed-sups-preserving

      proof

        let D be Subset of L such that

         A6: D is non empty directed and ex_sup_of (D,L);

        consider e be object such that

         A7: e in D by A6, XBOOLE_0:def 1;

        set S = { [(k . x), x] where x be Element of L : x in D };

        

         A8: S c= R

        proof

          let x be object;

          assume x in S;

          then

          consider a be Element of L such that

           A9: x = [(k . a), a] and a in D;

          (k . a) = ( inf ( Class (( EqRel R),a))) by A2, Def3;

          hence thesis by A2, A9, Th35;

        end;

        then

        reconsider S9 = S as Subset of ( subrelstr R) by YELLOW_0:def 15;

        reconsider S as Subset of [:L, L:] by A8, XBOOLE_1: 1;

        thus ex_sup_of ((k .: D),L) by YELLOW_0: 17;

        set d = ( sup D);

        set ds = ( sup (k .: D));

        

         A10: the carrier of ( subrelstr R) = R & ex_sup_of (S, [:L, L:]) by YELLOW_0: 17, YELLOW_0:def 15;

        reconsider e as Element of L by A7;

        

         A11: [(k . e), e] in S by A7;

        

         A12: S9 is directed

        proof

          let x,y be Element of ( subrelstr R);

          assume that

           A13: x in S9 and

           A14: y in S9;

          consider a be Element of L such that

           A15: x = [(k . a), a] and

           A16: a in D by A13;

          consider b be Element of L such that

           A17: y = [(k . b), b] and

           A18: b in D by A14;

          consider c be Element of L such that

           A19: c in D and

           A20: a <= c and

           A21: b <= c by A6, A16, A18;

          set z = [(k . c), c];

          z in S9 by A19;

          then

          reconsider z as Element of ( subrelstr R);

          take z;

          thus z in S9 by A19;

          (k . a) <= (k . c) by A20, WAYBEL_1:def 2;

          then [(k . a), a] <= [(k . c), c] by A20, YELLOW_3: 11;

          hence x <= z by A15, YELLOW_0: 60;

          (k . b) <= (k . c) by A21, WAYBEL_1:def 2;

          then [(k . b), b] <= [(k . c), c] by A21, YELLOW_3: 11;

          hence y <= z by A17, YELLOW_0: 60;

        end;

        now

          let x be object;

          hereby

            assume x in ( proj1 S);

            then

            consider y be object such that

             A22: [x, y] in S by XTUPLE_0:def 12;

            consider a be Element of L such that

             A23: [x, y] = [(k . a), a] and

             A24: a in D by A22;

            x = (k . a) by A23, XTUPLE_0: 1;

            hence x in (k .: D) by A1, A24, FUNCT_1:def 6;

          end;

          assume x in (k .: D);

          then

          consider y be object such that

           A25: y in ( dom k) and

           A26: y in D and

           A27: x = (k . y) by FUNCT_1:def 6;

          reconsider y as Element of L by A25;

           [(k . y), y] in S by A26;

          hence x in ( proj1 S) by A27, XTUPLE_0:def 12;

        end;

        then

         A28: ( proj1 S) = (k .: D) by TARSKI: 2;

        now

          let x be object;

          hereby

            assume x in ( proj2 S);

            then

            consider y be object such that

             A29: [y, x] in S by XTUPLE_0:def 13;

            ex a be Element of L st [y, x] = [(k . a), a] & a in D by A29;

            hence x in D by XTUPLE_0: 1;

          end;

          assume

           A30: x in D;

          then

          reconsider x9 = x as Element of L;

           [(k . x9), x9] in S by A30;

          hence x in ( proj2 S) by XTUPLE_0:def 13;

        end;

        then ( proj2 S) = D by TARSKI: 2;

        then ( sup S) = [ds, d] by A28, Th8, YELLOW_0: 17;

        then [ds, d] in R by A5, A10, A11, A12, WAYBEL_0:def 4;

        then

         A31: ds in ( Class (( EqRel R),d)) by A4, EQREL_1: 19;

        (k .: D) is_<=_than (k . d)

        proof

          let b be Element of L;

          assume b in (k .: D);

          then

          consider a be object such that

           A32: a in ( dom k) and

           A33: a in D and

           A34: b = (k . a) by FUNCT_1:def 6;

          reconsider a as Element of L by A32;

          D is_<=_than d by YELLOW_0: 32;

          then a <= d by A33;

          hence b <= (k . d) by A34, WAYBEL_1:def 2;

        end;

        then

         A35: ds <= (k . d) by YELLOW_0: 32;

        (k . d) = ( inf ( Class (( EqRel R),d))) by A2, Def3;

        then (k . d) <= ds by A31, YELLOW_2: 22;

        hence thesis by A35, YELLOW_0:def 3;

      end;

      now

        let x be object;

        hereby

          assume

           A36: x in R;

          then x in the carrier of [:L, L:];

          then x in [:cL, cL:] by YELLOW_3:def 2;

          then

          consider x1,x2 be object such that

           A37: x1 in cL & x2 in cL and

           A38: x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1, x2 as Element of L by A37;

          

           A39: (k . x1) = ( inf ( Class (( EqRel R),x1))) & (k . x2) = ( inf ( Class (( EqRel R),x2))) by A2, Def3;

          x1 in ( Class (( EqRel R),x2)) by A4, A36, A38, EQREL_1: 19;

          then (k . x1) = (k . x2) by A39, EQREL_1: 23;

          then

           A40: [(k . x1), (k . x2)] in ( id cL) by RELAT_1:def 10;

          ( dom [:k, k:]) = [:( dom k), ( dom k):] by FUNCT_3:def 8;

          then

           A41: [x1, x2] in ( dom [:k, k:]) by A1, ZFMISC_1: 87;

          ( [:k, k:] . (x1,x2)) = [(k . x1), (k . x2)] by A1, FUNCT_3:def 8;

          hence x in ( [:k, k:] " ( id cL)) by A38, A40, A41, FUNCT_1:def 7;

        end;

        assume

         A42: x in ( [:k, k:] " ( id cL));

        then

         A43: ( [:k, k:] . x) in ( id cL) by FUNCT_1:def 7;

        x in ( dom [:k, k:]) by A42, FUNCT_1:def 7;

        then x in [:( dom k), ( dom k):] by FUNCT_3:def 8;

        then

        consider x1,x2 be object such that

         A44: x1 in ( dom k) & x2 in ( dom k) and

         A45: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Element of L by A44;

        ( [:k, k:] . (x1,x2)) = [(k . x1), (k . x2)] by A44, FUNCT_3:def 8;

        then

         A46: (k . x1) = (k . x2) by A43, A45, RELAT_1:def 10;

        (k . x1) = ( inf ( Class (( EqRel R),x1))) by A2, Def3;

        then [(k . x1), x1] in R by A2, Th35;

        then

         A47: [x1, (k . x1)] in R by A3, EQREL_1: 6;

        (k . x2) = ( inf ( Class (( EqRel R),x2))) by A2, Def3;

        then [(k . x2), x2] in R by A2, Th35;

        hence x in R by A3, A45, A46, A47, EQREL_1: 7;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: WAYBEL20:37

    

     Th37: for L be continuous complete LATTICE, R be Subset of [:L, L:], k be kernel Function of L, L st k is directed-sups-preserving & R = ( [:k, k:] " ( id the carrier of L)) holds ex LR be continuous complete strict LATTICE st the carrier of LR = ( Class ( EqRel R)) & the InternalRel of LR = { [( Class (( EqRel R),x)), ( Class (( EqRel R),y))] where x,y be Element of L : (k . x) <= (k . y) } & for g be Function of L, LR st for x be Element of L holds (g . x) = ( Class (( EqRel R),x)) holds g is CLHomomorphism of L, LR

    proof

      let L be continuous complete LATTICE, R be Subset of [:L, L:], k be kernel Function of L, L such that

       A1: k is directed-sups-preserving and

       A2: R = ( [:k, k:] " ( id the carrier of L));

      set ER = ( EqRel R);

      R is Equivalence_Relation of the carrier of L by A2, Th2;

      then

       A3: ER = R by Def1;

      reconsider rngk = ( rng k) as non empty set;

      defpred P[ set, set] means ex x,y be Element of L st $1 = ( Class (ER,x)) & $2 = ( Class (ER,y)) & (k . x) <= (k . y);

      set xx = the Element of L;

      set cL = the carrier of L;

      ( Class (ER,xx)) in ( Class ER) by EQREL_1:def 3;

      then

      reconsider CER = ( Class ER) as non empty Subset-Family of cL;

      consider LR be non empty strict RelStr such that

       A4: the carrier of LR = CER and

       A5: for a,b be Element of LR holds a <= b iff P[a, b] from YELLOW_0:sch 1;

      defpred P[ set, set] means ex a be Element of cL st $1 = ( Class (ER,a)) & $2 = (k . a);

      

       A6: ( dom k) = cL by FUNCT_2:def 1;

      

       A7: for x be Element of CER holds ex y be Element of rngk st P[x, y]

      proof

        let x be Element of CER;

        consider y be object such that

         A8: y in cL and

         A9: x = ( Class (ER,y)) by EQREL_1:def 3;

        reconsider y as Element of L by A8;

        reconsider ky = (k . y) as Element of rngk by A6, FUNCT_1:def 3;

        take ky;

        thus thesis by A9;

      end;

      consider f be Function of CER, rngk such that

       A10: for x be Element of CER holds P[x, (f . x)] from FUNCT_2:sch 3( A7);

      

       A11: ( dom [:k, k:]) = [:cL, cL:] by A6, FUNCT_3:def 8;

      

       A12: for a,b be Element of cL holds ( Class (ER,a)) = ( Class (ER,b)) iff (k . a) = (k . b)

      proof

        let a,b be Element of cL;

        hereby

          assume ( Class (ER,a)) = ( Class (ER,b));

          then a in ( Class (ER,b)) by EQREL_1: 23;

          then [a, b] in R by A3, EQREL_1: 19;

          then ( [:k, k:] . (a,b)) in ( id cL) by A2, FUNCT_1:def 7;

          then [(k . a), (k . b)] in ( id cL) by A6, FUNCT_3:def 8;

          hence (k . a) = (k . b) by RELAT_1:def 10;

        end;

        assume (k . a) = (k . b);

        then [(k . a), (k . b)] in ( id cL) by RELAT_1:def 10;

        then [a, b] in [:cL, cL:] & ( [:k, k:] . (a,b)) in ( id cL) by A6, FUNCT_3:def 8, ZFMISC_1:def 2;

        then [a, b] in ER by A2, A3, A11, FUNCT_1:def 7;

        then a in ( Class (ER,b)) by EQREL_1: 19;

        hence thesis by EQREL_1: 23;

      end;

      

       A13: for x be Element of L holds (f . ( Class (ER,x))) = (k . x)

      proof

        let x be Element of L;

        reconsider CERx = ( Class (ER,x)) as Element of CER by EQREL_1:def 3;

        ex a be Element of cL st CERx = ( Class (ER,a)) & (f . CERx) = (k . a) by A10;

        hence thesis by A12;

      end;

      

       A14: for x be Element of LR holds ex a be Element of L st x = ( Class (ER,a))

      proof

        let x be Element of LR;

        x in CER by A4;

        then

        consider a be object such that

         A15: a in cL and

         A16: x = ( Class (ER,a)) by EQREL_1:def 3;

        reconsider a as Element of L by A15;

        take a;

        thus thesis by A16;

      end;

      now

        let x1,x2 be object;

        assume that

         A17: x1 in CER and

         A18: x2 in CER and

         A19: (f . x1) = (f . x2);

        reconsider x19 = x1 as Element of LR by A4, A17;

        consider a be Element of L such that

         A20: x19 = ( Class (ER,a)) by A14;

        reconsider x29 = x2 as Element of LR by A4, A18;

        consider b be Element of L such that

         A21: x29 = ( Class (ER,b)) by A14;

        

         A22: (f . x29) = (k . b) by A13, A21;

        (f . x19) = (k . a) by A13, A20;

        hence x1 = x2 by A12, A19, A20, A21, A22;

      end;

      then

       A23: f is one-to-one by FUNCT_2: 19;

      set tIR = the InternalRel of LR;

      

       A24: ( dom f) = CER by FUNCT_2:def 1;

      reconsider f as Function of LR, ( Image k) by A4, YELLOW_0:def 15;

      now

        let y be object;

        hereby

          assume y in ( rng f);

          then

          consider x be object such that

           A25: x in ( dom f) and

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

          reconsider x as Element of LR by A25;

          consider a be Element of L such that

           A27: x = ( Class (ER,a)) by A14;

          (f . x) = (k . a) by A13, A27;

          hence y in rngk by A6, A26, FUNCT_1:def 3;

        end;

        assume y in rngk;

        then

        consider x be object such that

         A28: x in ( dom k) and

         A29: y = (k . x) by FUNCT_1:def 3;

        reconsider x as Element of L by A28;

        ( Class (ER,x)) in CER & (f . ( Class (ER,x))) = (k . x) by A13, EQREL_1:def 3;

        hence y in ( rng f) by A24, A29, FUNCT_1:def 3;

      end;

      then

       A30: the carrier of ( Image k) = rngk & ( rng f) = rngk by TARSKI: 2, YELLOW_0:def 15;

      for x,y be Element of LR holds x <= y iff (f . x) <= (f . y)

      proof

        let x,y be Element of LR;

        x in CER by A4;

        then

        consider a be object such that

         A31: a in cL and

         A32: x = ( Class (ER,a)) by EQREL_1:def 3;

        hereby

          assume x <= y;

          then

          consider c,d be Element of L such that

           A33: x = ( Class (ER,c)) & y = ( Class (ER,d)) and

           A34: (k . c) <= (k . d) by A5;

          (f . x) = (k . c) & (f . y) = (k . d) by A13, A33;

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

        end;

        reconsider a as Element of L by A31;

        assume

         A35: (f . x) <= (f . y);

        y in CER by A4;

        then

        consider b be object such that

         A36: b in cL and

         A37: y = ( Class (ER,b)) by EQREL_1:def 3;

        reconsider b as Element of L by A36;

        

         A38: (f . y) = (k . b) by A13, A37;

        (f . x) = (k . a) by A13, A32;

        then (k . a) <= (k . b) by A38, A35, YELLOW_0: 59;

        hence thesis by A5, A32, A37;

      end;

      then

       A39: f is isomorphic by A23, A30, WAYBEL_0: 66;

      then

       A40: (LR,( Image k)) are_isomorphic ;

      then (( Image k),LR) are_isomorphic by WAYBEL_1: 6;

      then

      reconsider LR as non empty strict Poset by Th15, Th16, Th17;

      ( Image k) is complete by WAYBEL_1: 54;

      then

      reconsider LR as complete non empty strict Poset by A40, Th18, WAYBEL_1: 6;

      reconsider LR as complete strict LATTICE;

      ( Image k) is continuous LATTICE by A1, WAYBEL15: 14;

      then

      reconsider LR as continuous complete strict LATTICE by A40, WAYBEL15: 9, WAYBEL_1: 6;

      reconsider f9 = (f qua Function " ) as Function of ( Image k), LR by A23, A30, FUNCT_2: 25;

      set IR = { [( Class (ER,x)), ( Class (ER,y))] where x,y be Element of L : (k . x) <= (k . y) };

      

       A41: f9 is isomorphic by A39, WAYBEL_0: 68;

      then

       A42: ( corestr k) is infs-preserving & f9 is infs-preserving by WAYBEL13: 20, WAYBEL_1: 56;

      take LR;

      thus the carrier of LR = ( Class ER) by A4;

      now

        let z be object;

        hereby

          assume

           A43: z in tIR;

          then

          consider a,b be object such that

           A44: a in CER & b in CER and

           A45: z = [a, b] by A4, ZFMISC_1:def 2;

          reconsider a, b as Element of LR by A4, A44;

          a <= b by A43, A45, ORDERS_2:def 5;

          then ex x,y be Element of L st a = ( Class (ER,x)) & b = ( Class (ER,y)) & (k . x) <= (k . y) by A5;

          hence z in IR by A45;

        end;

        assume z in IR;

        then

        consider x,y be Element of L such that

         A46: z = [( Class (ER,x)), ( Class (ER,y))] and

         A47: (k . x) <= (k . y);

        reconsider b = ( Class (ER,y)) as Element of LR by A4, EQREL_1:def 3;

        reconsider a = ( Class (ER,x)) as Element of LR by A4, EQREL_1:def 3;

        a <= b by A5, A47;

        hence z in tIR by A46, ORDERS_2:def 5;

      end;

      hence the InternalRel of LR = { [( Class (ER,x)), ( Class (ER,y))] where x,y be Element of L : (k . x) <= (k . y) } by TARSKI: 2;

      let g be Function of L, LR such that

       A48: for x be Element of L holds (g . x) = ( Class (ER,x));

      now

        let x be object;

        assume

         A49: x in cL;

        then

        reconsider x9 = x as Element of L;

        

         A50: (f . ( Class (ER,x9))) = (k . x9) & ( Class (ER,x9)) in CER by A13, EQREL_1:def 3;

        ( dom ( corestr k)) = cL by FUNCT_2:def 1;

        

        hence ((f9 * ( corestr k)) . x) = (f9 . (( corestr k) . x)) by A49, FUNCT_1: 13

        .= (f9 . (k . x)) by WAYBEL_1: 30

        .= ( Class (ER,x9)) by A24, A23, A50, FUNCT_1: 32

        .= (g . x) by A48;

      end;

      then

       A51: g = (f9 * ( corestr k)) by FUNCT_2: 12;

      

       A52: ( corestr k) is directed-sups-preserving by A1, Th22;

      reconsider f9 as sups-preserving Function of ( Image k), LR by A41, WAYBEL13: 20;

      f9 is directed-sups-preserving;

      then

       A53: g is directed-sups-preserving by A51, A52, WAYBEL15: 11;

      g is infs-preserving by A51, A42, Th25;

      hence thesis by A53, WAYBEL16:def 1;

    end;

    theorem :: WAYBEL20:38

    

     Th38: for L be continuous complete LATTICE, R be Subset of [:L, L:] st R is Equivalence_Relation of the carrier of L & ex LR be continuous complete LATTICE st the carrier of LR = ( Class ( EqRel R)) & for g be Function of L, LR st for x be Element of L holds (g . x) = ( Class (( EqRel R),x)) holds g is CLHomomorphism of L, LR holds ( subrelstr R) is CLSubFrame of [:L, L:]

    proof

      let L be continuous complete LATTICE, R be Subset of [:L, L:];

      assume R is Equivalence_Relation of the carrier of L;

      then

       A1: ( EqRel R) = R by Def1;

      set ER = ( EqRel R);

      given LR be continuous complete LATTICE such that

       A2: the carrier of LR = ( Class ( EqRel R)) and

       A3: for g be Function of L, LR st for x be Element of L holds (g . x) = ( Class (( EqRel R),x)) holds g is CLHomomorphism of L, LR;

      deffunc F( object) = ( Class (ER,$1));

      set CER = ( Class ER);

      set cL = the carrier of L, cLR = the carrier of LR;

      

       A4: for x be object st x in cL holds F(x) in CER by EQREL_1:def 3;

      consider g be Function of cL, CER such that

       A5: for x be object st x in cL holds (g . x) = F(x) from FUNCT_2:sch 2( A4);

      reconsider g as Function of L, LR by A2;

      set k = g;

      

       A6: ( dom g) = cL by FUNCT_2:def 1;

      now

        let x be object;

        hereby

          assume

           A7: x in R;

          then x in the carrier of [:L, L:];

          then x in [:cL, cL:] by YELLOW_3:def 2;

          then

          consider x1,x2 be object such that

           A8: x1 in cL & x2 in cL and

           A9: x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1, x2 as Element of L by A8;

          

           A10: (k . x1) = ( Class (( EqRel R),x1)) & (k . x2) = ( Class (( EqRel R),x2)) by A5;

          x1 in ( Class (( EqRel R),x2)) by A1, A7, A9, EQREL_1: 19;

          then (k . x1) = (k . x2) by A10, EQREL_1: 23;

          then

           A11: [(k . x1), (k . x2)] in ( id cLR) by RELAT_1:def 10;

          ( dom [:k, k:]) = [:( dom k), ( dom k):] by FUNCT_3:def 8;

          then

           A12: [x1, x2] in ( dom [:k, k:]) by A6, ZFMISC_1: 87;

          ( [:k, k:] . (x1,x2)) = [(k . x1), (k . x2)] by A6, FUNCT_3:def 8;

          hence x in ( [:k, k:] " ( id cLR)) by A9, A11, A12, FUNCT_1:def 7;

        end;

        assume

         A13: x in ( [:k, k:] " ( id cLR));

        then

         A14: ( [:k, k:] . x) in ( id cLR) by FUNCT_1:def 7;

        x in ( dom [:k, k:]) by A13, FUNCT_1:def 7;

        then x in [:( dom k), ( dom k):] by FUNCT_3:def 8;

        then

        consider x1,x2 be object such that

         A15: x1 in ( dom k) & x2 in ( dom k) and

         A16: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Element of L by A15;

        

         A17: (k . x1) = ( Class (( EqRel R),x1)) & (k . x2) = ( Class (( EqRel R),x2)) by A5;

        ( [:k, k:] . (x1,x2)) = [(k . x1), (k . x2)] by A15, FUNCT_3:def 8;

        then (k . x1) = (k . x2) by A14, A16, RELAT_1:def 10;

        then x1 in ( Class (ER,x2)) by A17, EQREL_1: 23;

        hence x in R by A1, A16, EQREL_1: 19;

      end;

      then

       A18: R = ( [:g, g:] " ( id the carrier of LR)) by TARSKI: 2;

      for x be Element of L holds (g . x) = ( Class (( EqRel R),x)) by A5;

      then g is CLHomomorphism of L, LR by A3;

      hence thesis by A18, Th34;

    end;

    registration

      let L be non empty reflexive RelStr;

      cluster directed-sups-preserving kernel for Function of L, L;

      existence

      proof

        reconsider k = ( id L) as directed-sups-preserving kernel Function of L, L;

        take k;

        thus thesis;

      end;

    end

    definition

      let L be non empty reflexive RelStr, k be kernel Function of L, L;

      :: WAYBEL20:def4

      func kernel_congruence k -> non empty Subset of [:L, L:] equals ( [:k, k:] " ( id the carrier of L));

      coherence

      proof

        set cL = the carrier of L;

        set x = the Element of cL;

        

         A1: ( dom k) = cL by FUNCT_2:def 1;

        then

         A2: [(k . x), (k . x)] in ( id cL) & ( [:k, k:] . (x,x)) = [(k . x), (k . x)] by FUNCT_3:def 8, RELAT_1:def 10;

        ( dom [:k, k:]) = [:( dom k), ( dom k):] by FUNCT_3:def 8;

        then [x, x] in ( dom [:k, k:]) by A1, ZFMISC_1:def 2;

        hence thesis by A2, FUNCT_1:def 7;

      end;

    end

    theorem :: WAYBEL20:39

    for L be non empty reflexive RelStr, k be kernel Function of L, L holds ( kernel_congruence k) is Equivalence_Relation of the carrier of L by Th2;

    theorem :: WAYBEL20:40

    

     Th40: for L be continuous complete LATTICE, k be directed-sups-preserving kernel Function of L, L holds ( kernel_congruence k) is CLCongruence

    proof

      let L be continuous complete LATTICE, k be directed-sups-preserving kernel Function of L, L;

      set R = ( kernel_congruence k);

      thus

       A1: R is Equivalence_Relation of the carrier of L by Th2;

      ex LR be continuous complete strict LATTICE st the carrier of LR = ( Class ( EqRel R)) & the InternalRel of LR = { [( Class (( EqRel R),x)), ( Class (( EqRel R),y))] where x,y be Element of L : (k . x) <= (k . y) } & for g be Function of L, LR st for x be Element of L holds (g . x) = ( Class (( EqRel R),x)) holds g is CLHomomorphism of L, LR by Th37;

      hence thesis by A1, Th38;

    end;

    definition

      let L be continuous complete LATTICE, R be non empty Subset of [:L, L:];

      :: WAYBEL20:def5

      func L ./. R -> continuous complete strict LATTICE means

      : Def5: the carrier of it = ( Class ( EqRel R)) & for x,y be Element of it holds x <= y iff ( "/\" (x,L)) <= ( "/\" (y,L));

      existence

      proof

        set k = ( kernel_op R);

        k is directed-sups-preserving & R = ( [:k, k:] " ( id the carrier of L)) by A1, Th36;

        then

        consider LR be continuous complete strict LATTICE such that

         A2: the carrier of LR = ( Class ( EqRel R)) and

         A3: the InternalRel of LR = { [( Class (( EqRel R),x)), ( Class (( EqRel R),y))] where x,y be Element of L : (k . x) <= (k . y) } and for g be Function of L, LR st for x be Element of L holds (g . x) = ( Class (( EqRel R),x)) holds g is CLHomomorphism of L, LR by Th37;

        take LR;

        thus the carrier of LR = ( Class ( EqRel R)) by A2;

        let x,y be Element of LR;

        x in the carrier of LR;

        then

        consider u be object such that

         A4: u in the carrier of L and

         A5: x = ( Class (( EqRel R),u)) by A2, EQREL_1:def 3;

        y in the carrier of LR;

        then

        consider v be object such that

         A6: v in the carrier of L and

         A7: y = ( Class (( EqRel R),v)) by A2, EQREL_1:def 3;

        hereby

          assume x <= y;

          then [x, y] in the InternalRel of LR by ORDERS_2:def 5;

          then

          consider u9,v9 be Element of L such that

           A8: [x, y] = [( Class (( EqRel R),u9)), ( Class (( EqRel R),v9))] and

           A9: (k . u9) <= (k . v9) by A3;

          

           A10: x = ( Class (( EqRel R),u9)) & y = ( Class (( EqRel R),v9)) by A8, XTUPLE_0: 1;

          (k . u9) = ( inf ( Class (( EqRel R),u9))) by A1, Def3;

          hence ( "/\" (x,L)) <= ( "/\" (y,L)) by A1, A9, A10, Def3;

        end;

        assume

         A11: ( "/\" (x,L)) <= ( "/\" (y,L));

        reconsider u, v as Element of L by A4, A6;

        (k . u) = ( inf ( Class (( EqRel R),u))) & (k . v) = ( inf ( Class (( EqRel R),v))) by A1, Def3;

        then [x, y] in the InternalRel of LR by A3, A5, A7, A11;

        hence thesis by ORDERS_2:def 5;

      end;

      uniqueness

      proof

        let LR1,LR2 be continuous complete strict LATTICE such that

         A12: the carrier of LR1 = ( Class ( EqRel R)) and

         A13: for x,y be Element of LR1 holds x <= y iff ( "/\" (x,L)) <= ( "/\" (y,L)) and

         A14: the carrier of LR2 = ( Class ( EqRel R)) and

         A15: for x,y be Element of LR2 holds x <= y iff ( "/\" (x,L)) <= ( "/\" (y,L));

        set cLR2 = the carrier of LR2;

        set cLR1 = the carrier of LR1;

        now

          let z be object;

          hereby

            assume

             A16: z in the InternalRel of LR1;

            then

            consider x,y be object such that

             A17: x in cLR1 & y in cLR1 and

             A18: z = [x, y] by ZFMISC_1:def 2;

            reconsider x, y as Element of LR1 by A17;

            reconsider x9 = x, y9 = y as Element of LR2 by A12, A14;

            x <= y by A16, A18, ORDERS_2:def 5;

            then ( "/\" (x,L)) <= ( "/\" (y,L)) by A13;

            then x9 <= y9 by A15;

            hence z in the InternalRel of LR2 by A18, ORDERS_2:def 5;

          end;

          assume

           A19: z in the InternalRel of LR2;

          then

          consider x,y be object such that

           A20: x in cLR2 & y in cLR2 and

           A21: z = [x, y] by ZFMISC_1:def 2;

          reconsider x, y as Element of LR2 by A20;

          reconsider x9 = x, y9 = y as Element of LR1 by A12, A14;

          x <= y by A19, A21, ORDERS_2:def 5;

          then ( "/\" (x,L)) <= ( "/\" (y,L)) by A15;

          then x9 <= y9 by A13;

          hence z in the InternalRel of LR1 by A21, ORDERS_2:def 5;

        end;

        hence thesis by A12, A14, TARSKI: 2;

      end;

    end

    theorem :: WAYBEL20:41

    for L be continuous complete LATTICE, R be non empty Subset of [:L, L:] st R is CLCongruence holds for x be set holds x is Element of (L ./. R) iff ex y be Element of L st x = ( Class (( EqRel R),y))

    proof

      let L be continuous complete LATTICE, R be non empty Subset of [:L, L:];

      assume R is CLCongruence;

      then

       A1: the carrier of (L ./. R) = ( Class ( EqRel R)) by Def5;

      let x be set;

      hereby

        assume x is Element of (L ./. R);

        then x in ( Class ( EqRel R)) by A1;

        then

        consider y be object such that

         A2: y in the carrier of L and

         A3: x = ( Class (( EqRel R),y)) by EQREL_1:def 3;

        reconsider y as Element of L by A2;

        take y;

        thus x = ( Class (( EqRel R),y)) by A3;

      end;

      given y be Element of L such that

       A4: x = ( Class (( EqRel R),y));

      thus thesis by A1, A4, EQREL_1:def 3;

    end;

    theorem :: WAYBEL20:42

    for L be continuous complete LATTICE, R be non empty Subset of [:L, L:] st R is CLCongruence holds R = ( kernel_congruence ( kernel_op R)) by Th36;

    theorem :: WAYBEL20:43

    for L be continuous complete LATTICE, k be directed-sups-preserving kernel Function of L, L holds k = ( kernel_op ( kernel_congruence k))

    proof

      let L be continuous complete LATTICE, k be directed-sups-preserving kernel Function of L, L;

      set kc = ( kernel_congruence k), cL = the carrier of L, km = ( kernel_op kc);

      

       A1: ( dom k) = cL by FUNCT_2:def 1;

      

       A2: km <= ( id L) by WAYBEL_1:def 15;

      

       A3: k <= ( id L) by WAYBEL_1:def 15;

      

       A4: kc is CLCongruence by Th40;

      then

       A5: kc = ( [:km, km:] " ( id cL)) by Th36;

      reconsider kc9 = kc as Equivalence_Relation of cL by A4;

      ( field kc9) = cL by ORDERS_1: 12;

      then

       A6: kc9 is_transitive_in cL by RELAT_2:def 16;

      

       A7: ( dom [:km, km:]) = [:( dom km), ( dom km):] by FUNCT_3:def 8;

      

       A8: ( dom km) = cL by FUNCT_2:def 1;

      

       A9: ( dom [:k, k:]) = [:( dom k), ( dom k):] by FUNCT_3:def 8;

      now

        let x be object;

        assume x in cL;

        then

        reconsider x9 = x as Element of L;

        

         A10: (k . (k . x9)) = ((k * k) . x9) by A1, FUNCT_1: 13

        .= (k . x9) by QUANTAL1:def 9;

        

         A11: [(k . x9), (k . x9)] in ( id cL) & ( [:k, k:] . ((k . x9),x9)) = [(k . (k . x9)), (k . x9)] by A1, FUNCT_3:def 8, RELAT_1:def 10;

         [(k . x9), x9] in ( dom [:k, k:]) by A1, A9, ZFMISC_1:def 2;

        then

         A12: [(k . x9), x9] in kc by A10, A11, FUNCT_1:def 7;

        

         A13: (km . (km . x9)) = ((km * km) . x9) by A8, FUNCT_1: 13

        .= (km . x9) by QUANTAL1:def 9;

        (km . (k . x9)) <= (( id L) . (k . x9)) by A2, YELLOW_2: 9;

        then

         A14: (km . (k . x9)) <= (k . x9) by FUNCT_1: 18;

        

         A15: [(km . x9), (km . x9)] in ( id cL) & ( [:km, km:] . (x9,(km . x9))) = [(km . x9), (km . (km . x9))] by A8, FUNCT_3:def 8, RELAT_1:def 10;

         [x9, (km . x9)] in ( dom [:km, km:]) by A8, A7, ZFMISC_1:def 2;

        then [x9, (km . x9)] in kc by A5, A13, A15, FUNCT_1:def 7;

        then

         A16: [(k . x9), (km . x9)] in kc by A6, A12;

        then ( [:k, k:] . ((k . x9),(km . x9))) in ( id cL) by FUNCT_1:def 7;

        then [(k . (k . x9)), (k . (km . x9))] in ( id cL) by A1, FUNCT_3:def 8;

        

        then

         A17: (k . (km . x9)) = (k . (k . x9)) by RELAT_1:def 10

        .= ((k * k) . x9) by A1, FUNCT_1: 13

        .= (k . x9) by QUANTAL1:def 9;

        ( [:km, km:] . ((k . x9),(km . x9))) in ( id cL) by A5, A16, FUNCT_1:def 7;

        then [(km . (k . x9)), (km . (km . x9))] in ( id cL) by A8, FUNCT_3:def 8;

        

        then

         A18: (km . (k . x9)) = (km . (km . x9)) by RELAT_1:def 10

        .= ((km * km) . x9) by A8, FUNCT_1: 13

        .= (km . x9) by QUANTAL1:def 9;

        (k . (km . x9)) <= (( id L) . (km . x9)) by A3, YELLOW_2: 9;

        then (k . (km . x9)) <= (km . x9) by FUNCT_1: 18;

        hence (k . x) = (km . x) by A17, A18, A14, YELLOW_0:def 3;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: WAYBEL20:44

    for L be continuous complete LATTICE, p be projection Function of L, L st p is infs-preserving holds ( Image p) is continuous LATTICE & ( Image p) is infs-inheriting

    proof

      let L be continuous complete LATTICE, p be projection Function of L, L such that

       A1: p is infs-preserving;

      reconsider Lc = { c where c be Element of L : c <= (p . c) } as non empty Subset of L by WAYBEL_1: 43;

      reconsider pc = (p | Lc) as Function of ( subrelstr Lc), ( subrelstr Lc) by WAYBEL_1: 45;

      

       A2: ( subrelstr Lc) is infs-inheriting by A1, WAYBEL_1: 51;

      then

       A3: ( subrelstr Lc) is complete by YELLOW_2: 30;

      

       A4: pc is infs-preserving

      proof

        let X be Subset of ( subrelstr Lc);

        assume ex_inf_of (X,( subrelstr Lc));

        thus ex_inf_of ((pc .: X),( subrelstr Lc)) by A3, YELLOW_0: 17;

        the carrier of ( subrelstr Lc) = Lc by YELLOW_0:def 15;

        then

        reconsider X9 = X as Subset of L by XBOOLE_1: 1;

        

         A5: ex_inf_of (X9,L) & p preserves_inf_of X9 by A1, YELLOW_0: 17;

        X c= the carrier of ( subrelstr Lc);

        then X c= Lc by YELLOW_0:def 15;

        then

         A6: (pc .: X) = (p .: X) by RELAT_1: 129;

        

         A7: ex_inf_of (X,L) by YELLOW_0: 17;

        then ( "/\" (X9,L)) in the carrier of ( subrelstr Lc) by A2;

        then

         A8: ( dom pc) = the carrier of ( subrelstr Lc) & ( inf X9) = ( inf X) by A7, FUNCT_2:def 1, YELLOW_0: 63;

         ex_inf_of ((p .: X),L) & ( "/\" ((pc .: X),L)) in the carrier of ( subrelstr Lc) by A2, YELLOW_0: 17;

        

        hence ( inf (pc .: X)) = ( inf (p .: X)) by A6, YELLOW_0: 63

        .= (p . ( inf X9)) by A5

        .= (pc . ( inf X)) by A8, FUNCT_1: 47;

      end;

      reconsider cpc = ( corestr pc) as Function of ( subrelstr Lc), ( Image pc);

      

       A9: the carrier of ( subrelstr ( rng p)) = ( rng p) by YELLOW_0:def 15

      .= ( rng pc) by WAYBEL_1: 44

      .= the carrier of ( subrelstr ( rng pc)) by YELLOW_0:def 15;

      ( subrelstr ( rng pc)) is full SubRelStr of L by WAYBEL15: 1;

      then

       A10: ( Image p) = ( Image pc) by A9, YELLOW_0: 57;

      pc is closure by WAYBEL_1: 47;

      then

       A11: cpc is sups-preserving by WAYBEL_1: 55;

      ( subrelstr Lc) is sups-inheriting SubRelStr of L by WAYBEL_1: 49;

      then ( subrelstr Lc) is continuous LATTICE by A2, WAYBEL_5: 28;

      hence ( Image p) is continuous LATTICE by A3, A10, A4, A11, Th19, WAYBEL_5: 33;

      thus thesis by A1, A2, WAYBEL_1: 51;

    end;