waybel34.miz



    begin

    registration

      let S,T be complete LATTICE;

      cluster Galois for Connection of S, T;

      existence

      proof

        set g = the infs-preserving Function of S, T;

        g is upper_adjoint by WAYBEL_1: 16;

        then ex d be Function of T, S st [g, d] is Galois;

        hence thesis;

      end;

    end

    theorem :: WAYBEL34:1

    

     Th1: for S,T,S9,T9 be non empty RelStr st the RelStr of S = the RelStr of S9 & the RelStr of T = the RelStr of T9 holds for c be Connection of S, T, c9 be Connection of S9, T9 st c = c9 holds c is Galois implies c9 is Galois

    proof

      let S,T,S9,T9 be non empty RelStr such that

       A1: the RelStr of S = the RelStr of S9 and

       A2: the RelStr of T = the RelStr of T9;

      let c be Connection of S, T, c9 be Connection of S9, T9 such that

       A3: c = c9;

      given g be Function of S, T, d be Function of T, S such that

       A4: c = [g, d] and

       A5: g is monotone and

       A6: d is monotone and

       A7: for t be Element of T, s be Element of S holds t <= (g . s) iff (d . t) <= s;

      reconsider g9 = g as Function of S9, T9 by A1, A2;

      reconsider d9 = d as Function of T9, S9 by A1, A2;

      take g9, d9;

      thus c9 = [g9, d9] by A3, A4;

      thus g9 is monotone & d9 is monotone by A1, A2, A5, A6, WAYBEL_9: 1;

      let t9 be Element of T9, s9 be Element of S9;

      reconsider t = t9 as Element of T by A2;

      reconsider s = s9 as Element of S by A1;

      

       A8: t9 <= (g9 . s9) iff t <= (g . s) by A2, YELLOW_0: 1;

      (d9 . t9) <= s9 iff (d . t) <= s by A1, YELLOW_0: 1;

      hence thesis by A7, A8;

    end;

    definition

      let S,T be LATTICE;

      let g be Function of S, T;

      assume that

       A1: S is complete and

       A2: g is infs-preserving;

      

       A3: g is upper_adjoint by A1, A2, WAYBEL_1: 16;

      :: WAYBEL34:def1

      func LowerAdj g -> Function of T, S means

      : Def1: [g, it ] is Galois;

      uniqueness

      proof

        let d1,d2 be Function of T, S such that

         A4: [g, d1] is Galois and

         A5: [g, d2] is Galois;

        now

          let t be Element of T;

          reconsider t9 = t as Element of T;

          

           A6: (d1 . t9) is_minimum_of (g " ( uparrow t)) by A4, WAYBEL_1: 10;

          

           A7: (d2 . t9) is_minimum_of (g " ( uparrow t)) by A5, WAYBEL_1: 10;

          (d1 . t) = ( "/\" ((g " ( uparrow t)),S)) by A6;

          hence (d1 . t) = (d2 . t) by A7;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      existence by A3;

    end

    definition

      let S,T be LATTICE;

      let d be Function of T, S;

      assume that

       A1: T is complete and

       A2: d is sups-preserving;

      

       A3: d is lower_adjoint by A1, A2, WAYBEL_1: 17;

      :: WAYBEL34:def2

      func UpperAdj d -> Function of S, T means

      : Def2: [it , d] is Galois;

      existence by A3;

      correctness

      proof

        let g1,g2 be Function of S, T such that

         A4: [g1, d] is Galois and

         A5: [g2, d] is Galois;

        now

          let t be Element of S;

          reconsider t9 = t as Element of S;

          

           A6: (g1 . t9) is_maximum_of (d " ( downarrow t)) by A4, WAYBEL_1: 11;

          

           A7: (g2 . t9) is_maximum_of (d " ( downarrow t)) by A5, WAYBEL_1: 11;

          (g1 . t) = ( "\/" ((d " ( downarrow t)),T)) by A6;

          hence (g1 . t) = (g2 . t) by A7;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

     Lm1:

    now

      let S,T be LATTICE;

      assume that

       A1: S is complete and

       A2: T is complete;

      reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;

      let g be Function of S, T;

      assume g is infs-preserving;

      then

      reconsider g9 = g as infs-preserving Function of S9, T9;

       [g9, ( LowerAdj g9)] is Galois by Def1;

      then ( LowerAdj g9) is lower_adjoint monotone by WAYBEL_1: 8;

      hence ( LowerAdj g) is monotone lower_adjoint sups-preserving;

    end;

     Lm2:

    now

      let S,T be LATTICE;

      assume that

       A1: S is complete and

       A2: T is complete;

      reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;

      let g be Function of S, T;

      assume g is sups-preserving;

      then

      reconsider g9 = g as sups-preserving Function of S9, T9;

       [( UpperAdj g9), g9] is Galois by Def2;

      then ( UpperAdj g9) is upper_adjoint monotone by WAYBEL_1: 8;

      hence ( UpperAdj g) is monotone upper_adjoint infs-preserving;

    end;

    registration

      let S,T be complete LATTICE;

      let g be infs-preserving Function of S, T;

      cluster ( LowerAdj g) -> lower_adjoint;

      coherence by Lm1;

    end

    registration

      let S,T be complete LATTICE;

      let d be sups-preserving Function of T, S;

      cluster ( UpperAdj d) -> upper_adjoint;

      coherence by Lm2;

    end

    theorem :: WAYBEL34:2

    for S,T be complete LATTICE holds for g be infs-preserving Function of S, T holds for t be Element of T holds (( LowerAdj g) . t) = ( inf (g " ( uparrow t)))

    proof

      let S,T be complete LATTICE;

      let g be infs-preserving Function of S, T;

      let t be Element of T;

       [g, ( LowerAdj g)] is Galois by Def1;

      then (( LowerAdj g) . t) is_minimum_of (g " ( uparrow t)) by WAYBEL_1: 10;

      hence thesis;

    end;

    theorem :: WAYBEL34:3

    for S,T be complete LATTICE holds for d be sups-preserving Function of T, S holds for s be Element of S holds (( UpperAdj d) . s) = ( sup (d " ( downarrow s)))

    proof

      let S,T be complete LATTICE;

      let d be sups-preserving Function of T, S;

      let s be Element of S;

       [( UpperAdj d), d] is Galois by Def2;

      then (( UpperAdj d) . s) is_maximum_of (d " ( downarrow s)) by WAYBEL_1: 11;

      hence thesis;

    end;

    definition

      let S,T be RelStr;

      let f be Function of the carrier of S, the carrier of T;

      :: WAYBEL34:def3

      func f opp -> Function of (S opp ), (T opp ) equals f;

      coherence ;

    end

    registration

      let S,T be complete LATTICE;

      let g be infs-preserving Function of S, T;

      cluster (g opp ) -> lower_adjoint;

      coherence

      proof

         [g, ( LowerAdj g)] is Galois by Def1;

        then [(( LowerAdj g) opp ), (g opp )] is Galois by YELLOW_7: 44;

        hence thesis;

      end;

    end

    registration

      let S,T be complete LATTICE;

      let d be sups-preserving Function of S, T;

      cluster (d opp ) -> upper_adjoint;

      coherence

      proof

         [( UpperAdj d), d] is Galois by Def2;

        then [(d opp ), (( UpperAdj d) opp )] is Galois by YELLOW_7: 44;

        hence thesis;

      end;

    end

    theorem :: WAYBEL34:4

    for S,T be complete LATTICE holds for g be infs-preserving Function of S, T holds ( LowerAdj g) = ( UpperAdj (g opp ))

    proof

      let S,T be complete LATTICE;

      let g be infs-preserving Function of S, T;

       [g, ( LowerAdj g)] is Galois by Def1;

      then [(( LowerAdj g) opp ), (g opp )] is Galois by YELLOW_7: 44;

      hence thesis by Def2;

    end;

    theorem :: WAYBEL34:5

    for S,T be complete LATTICE holds for d be sups-preserving Function of S, T holds ( LowerAdj (d opp )) = ( UpperAdj d)

    proof

      let S,T be complete LATTICE;

      let d be sups-preserving Function of S, T;

       [( UpperAdj d), d] is Galois by Def2;

      then [(d opp ), (( UpperAdj d) opp )] is Galois by YELLOW_7: 44;

      hence thesis by Def1;

    end;

    theorem :: WAYBEL34:6

    

     Th6: for L be non empty RelStr holds [( id L), ( id L)] is Galois

    proof

      let L be non empty RelStr;

      take g = ( id L), d = ( id L);

      thus [( id L), ( id L)] = [g, d] & g is monotone & d is monotone;

      let t,s be Element of L;

      (g . s) = s by FUNCT_1: 18;

      hence thesis by FUNCT_1: 18;

    end;

    theorem :: WAYBEL34:7

    

     Th7: for L be complete LATTICE holds ( LowerAdj ( id L)) = ( id L) & ( UpperAdj ( id L)) = ( id L)

    proof

      let L be complete LATTICE;

       [( id L), ( id L)] is Galois by Th6;

      hence thesis by Def1, Def2;

    end;

    theorem :: WAYBEL34:8

    

     Th8: for L1,L2,L3 be complete LATTICE holds for g1 be infs-preserving Function of L1, L2 holds for g2 be infs-preserving Function of L2, L3 holds ( LowerAdj (g2 * g1)) = (( LowerAdj g1) * ( LowerAdj g2))

    proof

      let L1,L2,L3 be complete LATTICE;

      let g1 be infs-preserving Function of L1, L2;

      let g2 be infs-preserving Function of L2, L3;

      

       A1: [g1, ( LowerAdj g1)] is Galois by Def1;

       [g2, ( LowerAdj g2)] is Galois by Def1;

      then

       A2: [(g2 * g1), (( LowerAdj g1) * ( LowerAdj g2))] is Galois by A1, WAYBEL15: 5;

      (g2 * g1) is infs-preserving by WAYBEL20: 25;

      hence thesis by A2, Def1;

    end;

    theorem :: WAYBEL34:9

    

     Th9: for L1,L2,L3 be complete LATTICE holds for d1 be sups-preserving Function of L1, L2 holds for d2 be sups-preserving Function of L2, L3 holds ( UpperAdj (d2 * d1)) = (( UpperAdj d1) * ( UpperAdj d2))

    proof

      let L1,L2,L3 be complete LATTICE;

      let d1 be sups-preserving Function of L1, L2;

      let d2 be sups-preserving Function of L2, L3;

      

       A1: [( UpperAdj d1), d1] is Galois by Def2;

       [( UpperAdj d2), d2] is Galois by Def2;

      then

       A2: [(( UpperAdj d1) * ( UpperAdj d2)), (d2 * d1)] is Galois by A1, WAYBEL15: 5;

      (d2 * d1) is sups-preserving by WAYBEL20: 27;

      hence thesis by A2, Def2;

    end;

    theorem :: WAYBEL34:10

    

     Th10: for S,T be complete LATTICE holds for g be infs-preserving Function of S, T holds ( UpperAdj ( LowerAdj g)) = g

    proof

      let S,T be complete LATTICE;

      let g be infs-preserving Function of S, T;

       [g, ( LowerAdj g)] is Galois by Def1;

      hence thesis by Def2;

    end;

    theorem :: WAYBEL34:11

    

     Th11: for S,T be complete LATTICE holds for d be sups-preserving Function of S, T holds ( LowerAdj ( UpperAdj d)) = d

    proof

      let S,T be complete LATTICE;

      let d be sups-preserving Function of S, T;

       [( UpperAdj d), d] is Galois by Def2;

      hence thesis by Def1;

    end;

    theorem :: WAYBEL34:12

    

     Th12: for C be non empty AltCatStr holds for a,b,f be object st f in (the Arrows of C . (a,b)) holds ex o1,o2 be Object of C st o1 = a & o2 = b & f in <^o1, o2^> & f is Morphism of o1, o2

    proof

      let C be non empty AltCatStr;

      let a,b,f be object;

      assume

       A1: f in (the Arrows of C . (a,b));

      then [a, b] in ( dom the Arrows of C) by FUNCT_1:def 2;

      then [a, b] in [:the carrier of C, the carrier of C:];

      then

      reconsider o1 = a, o2 = b as Object of C by ZFMISC_1: 87;

      take o1, o2;

      thus thesis by A1, ALTCAT_1:def 1;

    end;

    definition

      let W be non empty set;

      defpred L[ LATTICE] means $1 is complete;

      defpred P[ LATTICE, LATTICE, Function of $1, $2] means $3 is infs-preserving;

      given w be Element of W such that

       A1: w is non empty;

      :: WAYBEL34:def4

      func W -INF_category -> lattice-wise strict category means

      : Def4: (for x be LATTICE holds x is Object of it iff x is strict complete & the carrier of x in W) & for a,b be Object of it , f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff f is infs-preserving;

      existence

      proof

        reconsider w as non empty set by A1;

        set r = the upper-bounded well-ordering Order of w;

         RelStr (# w, r #) is complete;

        then

         A2: ex x be strict LATTICE st L[x] & the carrier of x in W;

        

         A3: for a,b,c be LATTICE st L[a] & L[b] & L[c] holds for f be Function of a, b, g be Function of b, c st P[a, b, f] & P[b, c, g] holds P[a, c, (g * f)] by WAYBEL20: 25;

        

         A4: for a be LATTICE st L[a] holds P[a, a, ( id a)];

        thus ex C be lattice-wise strict category st (for x be LATTICE holds x is Object of C iff x is strict & L[x] & the carrier of x in W) & for a,b be Object of C, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[( latt a), ( latt b), f] from YELLOW21:sch 3( A2, A3, A4);

      end;

      uniqueness

      proof

        let C1,C2 be lattice-wise strict category such that

         A5: for x be LATTICE holds x is Object of C1 iff x is strict & L[x] & the carrier of x in W and

         A6: for a,b be Object of C1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff f is infs-preserving and

         A7: for x be LATTICE holds x is Object of C2 iff x is strict & L[x] & the carrier of x in W and

         A8: for a,b be Object of C2, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff f is infs-preserving;

        defpred Q[ set, set, set] means ex L1,L2 be LATTICE, f be Function of L1, L2 st $1 = L1 & $2 = L2 & $3 = f & f is infs-preserving;

         A9:

        now

          let a,b be Object of C1;

          let f be monotone Function of ( latt a), ( latt b);

          f in <^a, b^> iff f is infs-preserving by A6;

          hence f in <^a, b^> iff Q[a, b, f];

        end;

         A10:

        now

          let a,b be Object of C2;

          let f be monotone Function of ( latt a), ( latt b);

          f in <^a, b^> iff f is infs-preserving by A8;

          hence f in <^a, b^> iff Q[a, b, f];

        end;

        for C1,C2 be lattice-wise category st (for x be LATTICE holds x is Object of C1 iff x is strict & L[x] & the carrier of x in W) & (for a,b be Object of C1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff Q[a, b, f]) & (for x be LATTICE holds x is Object of C2 iff x is strict & L[x] & the carrier of x in W) & (for a,b be Object of C2, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff Q[a, b, f]) holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW21:sch 5;

        hence thesis by A5, A7, A9, A10;

      end;

    end

    

     Lm3: for W be with_non-empty_element set holds for a,b be LATTICE, f be Function of a, b holds f in (the Arrows of (W -INF_category ) . (a,b)) iff a in the carrier of (W -INF_category ) & b in the carrier of (W -INF_category ) & a is complete & b is complete & f is infs-preserving

    proof

      let W be with_non-empty_element set;

      

       A1: ex x be non empty set st x in W by SETFAM_1:def 10;

      let a,b be LATTICE, f be Function of a, b;

      set A = (W -INF_category );

      hereby

        assume f in (the Arrows of A . (a,b));

        then

        consider o1,o2 be Object of A such that

         A2: o1 = a and

         A3: o2 = b and

         A4: f in <^o1, o2^> and f is Morphism of o1, o2 by Th12;

        reconsider g = f as Morphism of o1, o2 by A4;

        thus a in the carrier of A & b in the carrier of A by A2, A3;

        thus a is complete & b is complete by A1, A2, A3, Def4;

        ( @ g) = f by A4, YELLOW21:def 7;

        hence f is infs-preserving by A1, A2, A3, A4, Def4;

      end;

      assume that

       A5: a in the carrier of (W -INF_category ) and

       A6: b in the carrier of (W -INF_category );

      reconsider x = a, y = b as Object of A by A5, A6;

      

       A7: ( latt x) = a;

      

       A8: ( latt y) = b;

      assume that a is complete and b is complete and

       A9: f is infs-preserving;

      f in <^x, y^> by A1, A7, A8, A9, Def4;

      hence thesis by ALTCAT_1:def 1;

    end;

    definition

      let W be non empty set;

      defpred L[ LATTICE] means $1 is complete;

      defpred P[ LATTICE, LATTICE, Function of $1, $2] means $3 is sups-preserving;

      given w be Element of W such that

       A1: w is non empty;

      :: WAYBEL34:def5

      func W -SUP_category -> lattice-wise strict category means

      : Def5: (for x be LATTICE holds x is Object of it iff x is strict complete & the carrier of x in W) & for a,b be Object of it , f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff f is sups-preserving;

      existence

      proof

        reconsider w as non empty set by A1;

        set r = the upper-bounded well-ordering Order of w;

         RelStr (# w, r #) is complete;

        then

         A2: ex x be strict LATTICE st L[x] & the carrier of x in W;

        

         A3: for a,b,c be LATTICE st L[a] & L[b] & L[c] holds for f be Function of a, b, g be Function of b, c st P[a, b, f] & P[b, c, g] holds P[a, c, (g * f)] by WAYBEL20: 27;

        

         A4: for a be LATTICE st L[a] holds P[a, a, ( id a)];

        thus ex C be lattice-wise strict category st (for x be LATTICE holds x is Object of C iff x is strict & L[x] & the carrier of x in W) & for a,b be Object of C, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[( latt a), ( latt b), f] from YELLOW21:sch 3( A2, A3, A4);

      end;

      uniqueness

      proof

        let C1,C2 be lattice-wise strict category such that

         A5: for x be LATTICE holds x is Object of C1 iff x is strict & L[x] & the carrier of x in W and

         A6: for a,b be Object of C1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff f is sups-preserving and

         A7: for x be LATTICE holds x is Object of C2 iff x is strict & L[x] & the carrier of x in W and

         A8: for a,b be Object of C2, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff f is sups-preserving;

        defpred Q[ set, set, set] means ex L1,L2 be LATTICE, f be Function of L1, L2 st $1 = L1 & $2 = L2 & $3 = f & f is sups-preserving;

         A9:

        now

          let a,b be Object of C1;

          let f be monotone Function of ( latt a), ( latt b);

          f in <^a, b^> iff f is sups-preserving by A6;

          hence f in <^a, b^> iff Q[a, b, f];

        end;

         A10:

        now

          let a,b be Object of C2;

          let f be monotone Function of ( latt a), ( latt b);

          f in <^a, b^> iff f is sups-preserving by A8;

          hence f in <^a, b^> iff Q[a, b, f];

        end;

        for C1,C2 be lattice-wise category st (for x be LATTICE holds x is Object of C1 iff x is strict & L[x] & the carrier of x in W) & (for a,b be Object of C1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff Q[a, b, f]) & (for x be LATTICE holds x is Object of C2 iff x is strict & L[x] & the carrier of x in W) & (for a,b be Object of C2, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff Q[a, b, f]) holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW21:sch 5;

        hence thesis by A5, A7, A9, A10;

      end;

    end

    

     Lm4: for W be with_non-empty_element set holds for a,b be LATTICE, f be Function of a, b holds f in (the Arrows of (W -SUP_category ) . (a,b)) iff a in the carrier of (W -SUP_category ) & b in the carrier of (W -SUP_category ) & a is complete & b is complete & f is sups-preserving

    proof

      let W be with_non-empty_element set;

      

       A1: ex x be non empty set st x in W by SETFAM_1:def 10;

      let a,b be LATTICE, f be Function of a, b;

      set A = (W -SUP_category );

      hereby

        assume f in (the Arrows of A . (a,b));

        then

        consider o1,o2 be Object of A such that

         A2: o1 = a and

         A3: o2 = b and

         A4: f in <^o1, o2^> and f is Morphism of o1, o2 by Th12;

        reconsider g = f as Morphism of o1, o2 by A4;

        thus a in the carrier of A & b in the carrier of A by A2, A3;

        thus a is complete & b is complete by A1, A2, A3, Def5;

        ( @ g) = f by A4, YELLOW21:def 7;

        hence f is sups-preserving by A1, A2, A3, A4, Def5;

      end;

      assume that

       A5: a in the carrier of (W -SUP_category ) and

       A6: b in the carrier of (W -SUP_category );

      reconsider x = a, y = b as Object of A by A5, A6;

      

       A7: ( latt x) = a;

      

       A8: ( latt y) = b;

      assume that a is complete and b is complete and

       A9: f is sups-preserving;

      f in <^x, y^> by A1, A7, A8, A9, Def5;

      hence thesis by ALTCAT_1:def 1;

    end;

    registration

      let W be with_non-empty_element set;

      cluster (W -INF_category ) -> with_complete_lattices;

      coherence

      proof

        thus (W -INF_category ) is lattice-wise;

        let a be Object of (W -INF_category );

        

         A1: ex x be non empty set st x in W by SETFAM_1:def 10;

        a = ( latt a);

        hence thesis by A1, Def4;

      end;

      cluster (W -SUP_category ) -> with_complete_lattices;

      coherence

      proof

        thus (W -SUP_category ) is lattice-wise;

        let a be Object of (W -SUP_category );

        

         A2: ex x be non empty set st x in W by SETFAM_1:def 10;

        a = ( latt a);

        hence thesis by A2, Def5;

      end;

    end

    theorem :: WAYBEL34:13

    

     Th13: for W be with_non-empty_element set holds for L be LATTICE holds L is Object of (W -INF_category ) iff L is strict complete & the carrier of L in W

    proof

      let W be with_non-empty_element set;

      ex a be non empty set st a in W by SETFAM_1:def 10;

      hence thesis by Def4;

    end;

    theorem :: WAYBEL34:14

    

     Th14: for W be with_non-empty_element set holds for a,b be Object of (W -INF_category ) holds for f be set holds f in <^a, b^> iff f is infs-preserving Function of ( latt a), ( latt b)

    proof

      let W be with_non-empty_element set;

      let a,b be Object of (W -INF_category ), f be set;

      

       A1: ex a be non empty set st a in W by SETFAM_1:def 10;

      hereby

        assume

         A2: f in <^a, b^>;

        then

        reconsider g = f as Morphism of a, b;

        f = ( @ g) by A2, YELLOW21:def 7;

        hence f is infs-preserving Function of ( latt a), ( latt b) by A1, A2, Def4;

      end;

      thus thesis by A1, Def4;

    end;

    theorem :: WAYBEL34:15

    

     Th15: for W be with_non-empty_element set holds for L be LATTICE holds L is Object of (W -SUP_category ) iff L is strict complete & the carrier of L in W

    proof

      let W be with_non-empty_element set;

      ex a be non empty set st a in W by SETFAM_1:def 10;

      hence thesis by Def5;

    end;

    theorem :: WAYBEL34:16

    

     Th16: for W be with_non-empty_element set holds for a,b be Object of (W -SUP_category ) holds for f be set holds f in <^a, b^> iff f is sups-preserving Function of ( latt a), ( latt b)

    proof

      let W be with_non-empty_element set;

      let a,b be Object of (W -SUP_category ), f be set;

      

       A1: ex a be non empty set st a in W by SETFAM_1:def 10;

      hereby

        assume

         A2: f in <^a, b^>;

        then

        reconsider g = f as Morphism of a, b;

        f = ( @ g) by A2, YELLOW21:def 7;

        hence f is sups-preserving Function of ( latt a), ( latt b) by A1, A2, Def5;

      end;

      thus thesis by A1, Def5;

    end;

    theorem :: WAYBEL34:17

    

     Th17: for W be with_non-empty_element set holds the carrier of (W -INF_category ) = the carrier of (W -SUP_category )

    proof

      let W be with_non-empty_element set;

      

       A1: ex x be non empty set st x in W by SETFAM_1:def 10;

      thus the carrier of (W -INF_category ) c= the carrier of (W -SUP_category )

      proof

        let x be object;

        assume

         A2: x in the carrier of (W -INF_category );

        then

        reconsider x as LATTICE by YELLOW21:def 4;

        

         A3: x is strict complete by A1, A2, Def4;

        the carrier of x in W by A1, A2, Def4;

        then x is Object of (W -SUP_category ) by A3, Def5;

        hence thesis;

      end;

      let x be object;

      assume

       A4: x in the carrier of (W -SUP_category );

      then

      reconsider x as LATTICE by YELLOW21:def 4;

      

       A5: x is strict complete by A1, A4, Def5;

      the carrier of x in W by A1, A4, Def5;

      then x is Object of (W -INF_category ) by A5, Def4;

      hence thesis;

    end;

    definition

      let W be with_non-empty_element set;

      set A = (W -INF_category ), B = (W -SUP_category );

      deffunc O( LATTICE) = $1;

      deffunc F( LATTICE, LATTICE, Function of $1, $2) = ( LowerAdj $3);

      defpred P[ LATTICE, LATTICE, Function of $1, $2] means $1 is complete & $2 is complete & $3 is infs-preserving;

      defpred Q[ LATTICE, LATTICE, Function of $1, $2] means $1 is complete & $2 is complete & $3 is sups-preserving;

      

       A1: for a,b be LATTICE, f be Function of a, b holds f in (the Arrows of A . (a,b)) iff a in the carrier of A & b in the carrier of A & P[a, b, f] by Lm3;

      

       A2: for a,b be LATTICE, f be Function of a, b holds f in (the Arrows of B . (a,b)) iff a in the carrier of B & b in the carrier of B & Q[a, b, f] by Lm4;

      

       A3: for a be LATTICE st a in the carrier of A holds O(a) in the carrier of B by Th17;

      

       A4: for a,b be LATTICE, f be Function of a, b st P[a, b, f] holds F(a,b,f) is Function of O(b), O(a) & Q[ O(b), O(a), F(a,b,f)];

       A5:

      now

        let a be LATTICE;

        assume a in the carrier of A;

        then a is complete by YELLOW21:def 5;

        hence F(a,a,id) = ( id O(a)) by Th7;

      end;

      

       A6: for a,b,c be LATTICE, f be Function of a, b, g be Function of b, c st P[a, b, f] & P[b, c, g] holds F(a,c,*) = ( F(a,b,f) * F(b,c,g)) by Th8;

      :: WAYBEL34:def6

      func W LowerAdj -> contravariant strict Functor of (W -INF_category ), (W -SUP_category ) means

      : Def6: (for a be Object of (W -INF_category ) holds (it . a) = ( latt a)) & for a,b be Object of (W -INF_category ) st <^a, b^> <> {} holds for f be Morphism of a, b holds (it . f) = ( LowerAdj ( @ f));

      existence

      proof

        thus ex F be contravariant strict Functor of (W -INF_category ), (W -SUP_category ) st (for a be Object of (W -INF_category ) holds (F . a) = O(latt)) & for a,b be Object of (W -INF_category ) st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = F(latt,latt,@) from YELLOW21:sch 7( A1, A2, A3, A4, A5, A6);

      end;

      uniqueness

      proof

        let F,G be contravariant strict Functor of A, B such that

         A7: for a be Object of (W -INF_category ) holds (F . a) = ( latt a) and

         A8: for a,b be Object of (W -INF_category ) st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = ( LowerAdj ( @ f)) and

         A9: for a be Object of (W -INF_category ) holds (G . a) = ( latt a) and

         A10: for a,b be Object of (W -INF_category ) st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . f) = ( LowerAdj ( @ f));

         A11:

        now

          let a be Object of A;

          

          thus (F . a) = ( latt a) by A7

          .= (G . a) by A9;

        end;

        now

          let a,b be Object of A such that

           A12: <^a, b^> <> {} ;

          let f be Morphism of a, b;

          

          thus (F . f) = ( LowerAdj ( @ f)) by A8, A12

          .= (G . f) by A10, A12;

        end;

        hence thesis by A11, YELLOW18: 2;

      end;

      deffunc G( LATTICE, LATTICE, Function of $1, $2) = ( UpperAdj $3);

      

       A13: for a be LATTICE st a in the carrier of B holds O(a) in the carrier of A by Th17;

      

       A14: for a,b be LATTICE, f be Function of a, b st Q[a, b, f] holds G(a,b,f) is Function of O(b), O(a) & P[ O(b), O(a), G(a,b,f)];

       A15:

      now

        let a be LATTICE;

        assume a in the carrier of B;

        then a is complete by YELLOW21:def 5;

        hence G(a,a,id) = ( id O(a)) by Th7;

      end;

      

       A16: for a,b,c be LATTICE, f be Function of a, b, g be Function of b, c st Q[a, b, f] & Q[b, c, g] holds G(a,c,*) = ( G(a,b,f) * G(b,c,g)) by Th9;

      :: WAYBEL34:def7

      func W UpperAdj -> contravariant strict Functor of (W -SUP_category ), (W -INF_category ) means

      : Def7: (for a be Object of (W -SUP_category ) holds (it . a) = ( latt a)) & for a,b be Object of (W -SUP_category ) st <^a, b^> <> {} holds for f be Morphism of a, b holds (it . f) = ( UpperAdj ( @ f));

      existence

      proof

        thus ex F be contravariant strict Functor of B, A st (for a be Object of B holds (F . a) = O(latt)) & for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = G(latt,latt,@) from YELLOW21:sch 7( A2, A1, A13, A14, A15, A16);

      end;

      uniqueness

      proof

        let F,G be contravariant strict Functor of B, A such that

         A17: for a be Object of B holds (F . a) = ( latt a) and

         A18: for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = ( UpperAdj ( @ f)) and

         A19: for a be Object of B holds (G . a) = ( latt a) and

         A20: for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . f) = ( UpperAdj ( @ f));

         A21:

        now

          let a be Object of B;

          

          thus (F . a) = ( latt a) by A17

          .= (G . a) by A19;

        end;

        now

          let a,b be Object of B such that

           A22: <^a, b^> <> {} ;

          let f be Morphism of a, b;

          

          thus (F . f) = ( UpperAdj ( @ f)) by A18, A22

          .= (G . f) by A20, A22;

        end;

        hence thesis by A21, YELLOW18: 2;

      end;

    end

    registration

      let W be with_non-empty_element set;

      cluster (W LowerAdj ) -> bijective;

      coherence

      proof

        set A = (W -INF_category ), B = (W -SUP_category );

        set F = (W LowerAdj );

        

         A1: ex x be non empty set st x in W by SETFAM_1:def 10;

        deffunc O( Object of A) = ( latt $1);

        deffunc F( Object of A, Object of A, Morphism of $1, $2) = ( LowerAdj ( @ $3));

        

         A2: for a be Object of A holds (F . a) = O(a) by Def6;

        

         A3: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = F(a,b,f) by Def6;

        

         A4: for a,b be Object of A st O(a) = O(b) holds a = b;

         A5:

        now

          let a,b be Object of A such that

           A6: <^a, b^> <> {} ;

          let f,g be Morphism of a, b;

          

           A7: ( @ f) = f by A6, YELLOW21:def 7;

          

           A8: ( @ g) = g by A6, YELLOW21:def 7;

          

           A9: ( latt a) is complete;

          

           A10: ( latt b) is complete;

          

           A11: ( @ f) is infs-preserving by A1, A6, A7, Def4;

          

           A12: ( @ g) is infs-preserving by A1, A6, A8, Def4;

          assume F(a,b,f) = F(a,b,g);

          

          hence f = ( UpperAdj ( LowerAdj ( @ g))) by A7, A9, A10, A11, Th10

          .= g by A8, A9, A10, A12, Th10;

        end;

         A13:

        now

          let a,b be Object of B such that

           A14: <^a, b^> <> {} ;

          let f be Morphism of a, b;

          

           A15: ( latt a) is strict complete by A1, Def5;

          

           A16: the carrier of ( latt a) in W by A1, Def5;

          

           A17: ( latt b) is strict complete by A1, Def5;

          the carrier of ( latt b) in W by A1, Def5;

          then

          reconsider c = ( latt b), d = ( latt a) as Object of A by A15, A16, A17, Def4;

          take c, d;

          

           A18: ( latt c) = c;

          

           A19: ( latt d) = d;

          

           A20: f = ( @ f) by A14, YELLOW21:def 7;

          then

           A21: ( @ f) is sups-preserving by A1, A14, Def5;

          then

           A22: ( UpperAdj ( @ f)) is monotone infs-preserving by A18, A19;

          

           A23: ( UpperAdj ( @ f)) in <^c, d^> by A1, A21, Def4;

          reconsider g = ( UpperAdj ( @ f)) as Morphism of c, d by A1, A21, Def4;

          take g;

          thus b = O(c) & a = O(d) & <^c, d^> <> {} by A1, A22, Def4;

          g = ( @ g) by A23, YELLOW21:def 7;

          hence f = F(c,d,g) by A20, A21, Th11;

        end;

        thus thesis from YELLOW18:sch 12( A2, A3, A4, A5, A13);

      end;

      cluster (W UpperAdj ) -> bijective;

      coherence

      proof

        set A = (W -SUP_category ), B = (W -INF_category );

        set F = (W UpperAdj );

        

         A24: ex x be non empty set st x in W by SETFAM_1:def 10;

        deffunc O( Object of A) = ( latt $1);

        deffunc F( Object of A, Object of A, Morphism of $1, $2) = ( UpperAdj ( @ $3));

        

         A25: for a be Object of A holds (F . a) = O(a) by Def7;

        

         A26: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = F(a,b,f) by Def7;

        

         A27: for a,b be Object of A st O(a) = O(b) holds a = b;

         A28:

        now

          let a,b be Object of A such that

           A29: <^a, b^> <> {} ;

          let f,g be Morphism of a, b;

          

           A30: ( @ f) = f by A29, YELLOW21:def 7;

          

           A31: ( @ g) = g by A29, YELLOW21:def 7;

          

           A32: ( latt a) is complete;

          

           A33: ( latt b) is complete;

          

           A34: ( @ f) is sups-preserving by A24, A29, A30, Def5;

          

           A35: ( @ g) is sups-preserving by A24, A29, A31, Def5;

          assume F(a,b,f) = F(a,b,g);

          

          hence f = ( LowerAdj ( UpperAdj ( @ g))) by A30, A32, A33, A34, Th11

          .= g by A31, A32, A33, A35, Th11;

        end;

         A36:

        now

          let a,b be Object of B such that

           A37: <^a, b^> <> {} ;

          let f be Morphism of a, b;

          

           A38: ( latt a) is strict complete by A24, Def4;

          

           A39: the carrier of ( latt a) in W by A24, Def4;

          

           A40: ( latt b) is strict complete by A24, Def4;

          the carrier of ( latt b) in W by A24, Def4;

          then

          reconsider c = ( latt b), d = ( latt a) as Object of A by A38, A39, A40, Def5;

          take c, d;

          

           A41: ( latt c) = c;

          

           A42: ( latt d) = d;

          

           A43: f = ( @ f) by A37, YELLOW21:def 7;

          then

           A44: ( @ f) is infs-preserving by A24, A37, Def4;

          then

           A45: ( LowerAdj ( @ f)) is monotone sups-preserving by A41, A42;

          

           A46: ( LowerAdj ( @ f)) in <^c, d^> by A24, A44, Def5;

          reconsider g = ( LowerAdj ( @ f)) as Morphism of c, d by A24, A44, Def5;

          take g;

          thus b = O(c) & a = O(d) & <^c, d^> <> {} by A24, A45, Def5;

          g = ( @ g) by A46, YELLOW21:def 7;

          hence f = F(c,d,g) by A43, A44, Th10;

        end;

        thus thesis from YELLOW18:sch 12( A25, A26, A27, A28, A36);

      end;

    end

    theorem :: WAYBEL34:18

    

     Th18: for W be with_non-empty_element set holds ((W LowerAdj ) " ) = (W UpperAdj ) & ((W UpperAdj ) " ) = (W LowerAdj )

    proof

      let W be with_non-empty_element set;

      

       A1: ex x be non empty set st x in W by SETFAM_1:def 10;

      set B = (W -SUP_category );

      set F = (W LowerAdj ), G = (W UpperAdj );

       A2:

      now

        let a be Object of B;

        

        thus (F . (G . a)) = ( latt (G . a)) by Def6

        .= ( latt a) by Def7

        .= a;

      end;

      now

        let a,b be Object of B;

        assume

         A3: <^a, b^> <> {} ;

        then

         A4: <^(G . b), (G . a)^> <> {} by FUNCTOR0:def 19;

        let f be Morphism of a, b;

        

         A5: (G . f) = ( UpperAdj ( @ f)) by A3, Def7;

        

         A6: ( @ f) = f by A3, YELLOW21:def 7;

        

         A7: ( @ (G . f)) = (G . f) by A4, YELLOW21:def 7;

        

         A8: (G . a) = ( latt a) by Def7;

        

         A9: (G . b) = ( latt b) by Def7;

        

         A10: ( @ f) is sups-preserving by A1, A3, A6, Def5;

        

        thus (F . (G . f)) = ( LowerAdj ( @ (G . f))) by A4, Def6

        .= f by A5, A6, A7, A8, A9, A10, Th11;

      end;

      hence (F " ) = G by A2, YELLOW20: 7;

      set B = (W -INF_category );

      set G = (W LowerAdj ), F = (W UpperAdj );

       A11:

      now

        let a be Object of B;

        

        thus (F . (G . a)) = ( latt (G . a)) by Def7

        .= ( latt a) by Def6

        .= a;

      end;

      now

        let a,b be Object of B;

        assume

         A12: <^a, b^> <> {} ;

        then

         A13: <^(G . b), (G . a)^> <> {} by FUNCTOR0:def 19;

        let f be Morphism of a, b;

        

         A14: (G . f) = ( LowerAdj ( @ f)) by A12, Def6;

        

         A15: ( @ f) = f by A12, YELLOW21:def 7;

        

         A16: ( @ (G . f)) = (G . f) by A13, YELLOW21:def 7;

        

         A17: (G . a) = ( latt a) by Def6;

        

         A18: (G . b) = ( latt b) by Def6;

        

         A19: ( @ f) is infs-preserving by A1, A12, A15, Def4;

        

        thus (F . (G . f)) = ( UpperAdj ( @ (G . f))) by A13, Def7

        .= f by A14, A15, A16, A17, A18, A19, Th10;

      end;

      hence thesis by A11, YELLOW20: 7;

    end;

    theorem :: WAYBEL34:19

    for W be with_non-empty_element set holds ((W LowerAdj ) * (W UpperAdj )) = ( id (W -SUP_category )) & ((W UpperAdj ) * (W LowerAdj )) = ( id (W -INF_category ))

    proof

      let W be with_non-empty_element set;

      

       A1: ((W LowerAdj ) " ) = (W UpperAdj ) by Th18;

      ((W UpperAdj ) " ) = (W LowerAdj ) by Th18;

      hence thesis by A1, FUNCTOR1: 18;

    end;

    theorem :: WAYBEL34:20

    for W be with_non-empty_element set holds ((W -INF_category ),(W -SUP_category )) are_anti-isomorphic

    proof

      let W be with_non-empty_element set;

      take (W LowerAdj );

      thus thesis;

    end;

    begin

    theorem :: WAYBEL34:21

    

     Th21: for S,T be complete LATTICE, g be infs-preserving Function of S, T holds g is directed-sups-preserving iff for X be Scott TopAugmentation of T holds for Y be Scott TopAugmentation of S holds for V be open Subset of X holds ( uparrow (( LowerAdj g) .: V)) is open Subset of Y

    proof

      let S,T be complete LATTICE, g be infs-preserving Function of S, T;

      hereby

        assume

         A1: g is directed-sups-preserving;

        let X be Scott TopAugmentation of T;

        let Y be Scott TopAugmentation of S;

        let V be open Subset of X;

        

         A2: the RelStr of X = the RelStr of T by YELLOW_9:def 4;

        

         A3: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;

        then

        reconsider g9 = g as Function of Y, X by A2;

        reconsider d = ( LowerAdj g) as Function of X, Y by A2, A3;

        ( uparrow (d .: V)) is inaccessible

        proof

          let D be non empty directed Subset of Y;

          assume ( sup D) in ( uparrow (d .: V));

          then

          consider y be Element of Y such that

           A4: y <= ( sup D) and

           A5: y in (d .: V) by WAYBEL_0:def 16;

          consider u be object such that

           A6: u in the carrier of X and

           A7: u in V and

           A8: y = (d . u) by A5, FUNCT_2: 64;

          reconsider u as Element of X by A6;

          reconsider g = g9 as Function of Y, X;

           [g, d] is Galois Connection of S, T by Def1;

          then

           A9: [g, d] is Galois by A2, A3, Th1;

          then

           A10: (d * g) <= ( id Y) by WAYBEL_1: 18;

          

           A11: ( id X) <= (g * d) by A9, WAYBEL_1: 18;

          

           A12: (( id X) . u) = u by FUNCT_1: 18;

          

           A13: ((g * d) . u) = (g . (d . u)) by FUNCT_2: 15;

          

           A14: g is infs-preserving Function of Y, X by A2, A3, WAYBEL21: 6;

          

           A15: u <= (g . y) by A8, A11, A12, A13, YELLOW_2: 9;

          (g . y) <= (g . ( sup D)) by A4, A14, ORDERS_3:def 5;

          then

           A16: u <= (g . ( sup D)) by A15, ORDERS_2: 3;

          V is upper by WAYBEL11:def 4;

          then

           A17: (g . ( sup D)) in V by A7, A16;

          g is directed-sups-preserving by A1, A2, A3, WAYBEL21: 6;

          then

           A18: g preserves_sup_of D;

           ex_sup_of (D,Y) by YELLOW_0: 17;

          then

           A19: (g . ( sup D)) = ( sup (g .: D)) by A18;

          

           A20: (g .: D) is directed non empty by A14, YELLOW_2: 15;

          V is inaccessible by WAYBEL11:def 4;

          then (g .: D) meets V by A17, A19, A20;

          then

          consider z be object such that

           A21: z in (g .: D) and

           A22: z in V by XBOOLE_0: 3;

          consider x be object such that

           A23: x in the carrier of Y and

           A24: x in D and

           A25: z = (g qua Function . x) by A21, FUNCT_2: 64;

          reconsider x as Element of Y by A23;

          

           A26: ((d * g) . x) = (d . (g . x)) by FUNCT_2: 15;

          (( id Y) . x) = x by FUNCT_1: 18;

          then

           A27: (d . (g . x)) <= x by A10, A26, YELLOW_2: 9;

          (d . z) in (d .: V) by A22, FUNCT_2: 35;

          then x in ( uparrow (d .: V)) by A25, A27, WAYBEL_0:def 16;

          hence thesis by A24, XBOOLE_0: 3;

        end;

        then ( uparrow (d .: V)) is open Subset of Y by WAYBEL11:def 4;

        hence ( uparrow (( LowerAdj g) .: V)) is open Subset of Y by A3, WAYBEL_0: 13;

      end;

      assume

       A28: for X be Scott TopAugmentation of T holds for Y be Scott TopAugmentation of S holds for V be open Subset of X holds ( uparrow (( LowerAdj g) .: V)) is open Subset of Y;

      set X = the Scott TopAugmentation of T, Y = the Scott TopAugmentation of S;

      

       A29: the RelStr of X = the RelStr of T by YELLOW_9:def 4;

      

       A30: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;

      then

      reconsider g9 = g as Function of Y, X by A29;

      reconsider g9 as infs-preserving Function of Y, X by A29, A30, WAYBEL21: 6;

      set d = ( LowerAdj g);

      reconsider d9 = d as Function of X, Y by A29, A30;

      let D be Subset of S such that

       A31: D is non empty directed;

      assume ex_sup_of (D,S);

      thus ex_sup_of ((g .: D),T) by YELLOW_0: 17;

      

       A32: ( sup (g .: D)) <= (g . ( sup D)) by WAYBEL17: 15;

      reconsider D9 = D as Subset of Y by A30;

      reconsider D9 as non empty directed Subset of Y by A30, A31, WAYBEL_0: 3;

      reconsider s = ( sup D) as Element of Y by A30;

      set U9 = (( downarrow ( sup (g9 .: D9))) ` );

      

       A33: U9 is open by WAYBEL11: 12;

      then ( uparrow (d .: U9)) is open Subset of Y by A28;

      then

       A34: ( uparrow (d .: U9)) is upper inaccessible Subset of Y by WAYBEL11:def 4;

      ( sup (g9 .: D9)) = ( sup (g .: D)) by A29, YELLOW_0: 17, YELLOW_0: 26;

      then

       A35: ( downarrow ( sup (g9 .: D9))) = ( downarrow ( sup (g .: D))) by A29, WAYBEL_0: 13;

      

       A36: ( sup (g .: D)) <= ( sup (g .: D));

      

       A37: [g, d] is Galois by Def1;

      then

       A38: (d * g) <= ( id S) by WAYBEL_1: 18;

      

       A39: ( id T) <= (g * d) by A37, WAYBEL_1: 18;

      

       A40: (( id S) . ( sup D)) = ( sup D) by FUNCT_1: 18;

      ((d * g) . ( sup D)) = (d . (g . ( sup D))) by FUNCT_2: 15;

      then (d . (g . ( sup D))) <= ( sup D) by A38, A40, YELLOW_2: 9;

      then

       A41: (d9 . (g9 . s)) <= s by A30, YELLOW_0: 1;

      

       A42: s = ( sup D9) by A30, YELLOW_0: 17, YELLOW_0: 26;

      (g . ( sup D)) <= ( sup (g .: D))

      proof

        assume not thesis;

        then

         A43: not (g . ( sup D)) in ( downarrow ( sup (g .: D))) by WAYBEL_0: 17;

        

         A44: ( sup (g .: D)) in ( downarrow ( sup (g .: D))) by A36, WAYBEL_0: 17;

        

         A45: (g . ( sup D)) in U9 by A29, A35, A43, XBOOLE_0:def 5;

        

         A46: not ( sup (g .: D)) in U9 by A35, A44, XBOOLE_0:def 5;

        

         A47: (d9 . (g9 . s)) in (d9 .: U9) by A45, FUNCT_2: 35;

        (d9 .: U9) c= ( uparrow (d9 .: U9)) by WAYBEL_0: 16;

        then

         A48: s in ( uparrow (d9 .: U9)) by A41, A47, WAYBEL_0:def 20;

        ( uparrow (d9 .: U9)) = ( uparrow (d .: U9)) by A30, WAYBEL_0: 13;

        then D9 meets ( uparrow (d9 .: U9)) by A34, A42, A48, WAYBEL11:def 1;

        then

        consider x be object such that

         A49: x in D9 and

         A50: x in ( uparrow (d9 .: U9)) by XBOOLE_0: 3;

        reconsider x as Element of Y by A49;

        consider u9 be Element of Y such that

         A51: u9 <= x and

         A52: u9 in (d9 .: U9) by A50, WAYBEL_0:def 16;

        consider u be object such that

         A53: u in the carrier of X and

         A54: u in U9 and

         A55: u9 = (d9 . u) by A52, FUNCT_2: 64;

        reconsider u as Element of X by A53;

        reconsider a = u as Element of T by A29;

        (( id T) . a) = u by FUNCT_1: 18;

        then a <= ((g * d) . a) by A39, YELLOW_2: 9;

        then a <= (g . (d . a)) by FUNCT_2: 15;

        then

         A56: u <= (g9 . (d9 . u)) by A29, YELLOW_0: 1;

        (g9 . (d9 . u)) <= (g9 . x) by A51, A55, ORDERS_3:def 5;

        then

         A57: u <= (g9 . x) by A56, ORDERS_2: 3;

        (g9 . x) in (g9 .: D9) by A49, FUNCT_2: 35;

        then (g9 . x) <= ( sup (g9 .: D9)) by YELLOW_2: 22;

        then

         A58: u <= ( sup (g9 .: D9)) by A57, ORDERS_2: 3;

        U9 is upper by A33, WAYBEL11:def 4;

        then ( sup (g9 .: D9)) in U9 by A54, A58;

        hence thesis by A29, A46, YELLOW_0: 17, YELLOW_0: 26;

      end;

      hence thesis by A32, ORDERS_2: 2;

    end;

    definition

      let S,T be non empty reflexive RelStr;

      let f be Function of S, T;

      :: WAYBEL34:def8

      attr f is waybelow-preserving means for x,y be Element of S st x << y holds (f . x) << (f . y);

    end

    theorem :: WAYBEL34:22

    

     Th22: for S,T be complete LATTICE, g be infs-preserving Function of S, T holds g is directed-sups-preserving implies ( LowerAdj g) is waybelow-preserving

    proof

      let S,T be complete LATTICE, g be infs-preserving Function of S, T such that

       A1: g is directed-sups-preserving;

      set d = ( LowerAdj g);

      

       A2: [g, d] is Galois by Def1;

      let t,t9 be Element of T such that

       A3: t << t9;

      let D be non empty directed Subset of S;

      assume (d . t9) <= ( sup D);

      then

       A4: t9 <= (g . ( sup D)) by A2, WAYBEL_1: 8;

      

       A5: g preserves_sup_of D by A1;

       ex_sup_of (D,S) by YELLOW_0: 17;

      then

       A6: (g . ( sup D)) = ( sup (g .: D)) by A5;

      (g .: D) is directed non empty by YELLOW_2: 15;

      then

      consider x be Element of T such that

       A7: x in (g .: D) and

       A8: t <= x by A3, A4, A6;

      consider s be object such that

       A9: s in the carrier of S and

       A10: s in D and

       A11: x = (g . s) by A7, FUNCT_2: 64;

      reconsider s as Element of S by A9;

      take s;

      thus thesis by A2, A8, A10, A11, WAYBEL_1: 8;

    end;

    theorem :: WAYBEL34:23

    

     Th23: for S be complete LATTICE holds for T be complete continuous LATTICE holds for g be infs-preserving Function of S, T st ( LowerAdj g) is waybelow-preserving holds g is directed-sups-preserving

    proof

      let S be complete LATTICE;

      let T be complete continuous LATTICE;

      let g be infs-preserving Function of S, T such that

       A1: for t,t9 be Element of T st t << t9 holds (( LowerAdj g) . t) << (( LowerAdj g) . t9);

      let D be Subset of S;

      assume

       A2: D is non empty directed;

      assume ex_sup_of (D,S);

      thus ex_sup_of ((g .: D),T) by YELLOW_0: 17;

      

       A3: ( sup (g .: D)) <= (g . ( sup D)) by WAYBEL17: 15;

      

       A4: (g . ( sup D)) = ( sup ( waybelow (g . ( sup D)))) by WAYBEL_3:def 5;

      ( waybelow (g . ( sup D))) is_<=_than ( sup (g .: D))

      proof

        let t be Element of T;

        assume t in ( waybelow (g . ( sup D)));

        then t << (g . ( sup D)) by WAYBEL_3: 7;

        then

         A5: (( LowerAdj g) . t) << (( LowerAdj g) . (g . ( sup D))) by A1;

        

         A6: [g, ( LowerAdj g)] is Galois by Def1;

        then

         A7: (( LowerAdj g) * g) <= ( id S) by WAYBEL_1: 18;

        (( id S) . ( sup D)) = ( sup D) by FUNCT_1: 18;

        then ((( LowerAdj g) * g) . ( sup D)) <= ( sup D) by A7, YELLOW_2: 9;

        then (( LowerAdj g) . (g . ( sup D))) <= ( sup D) by FUNCT_2: 15;

        then

        consider x be Element of S such that

         A8: x in D and

         A9: (( LowerAdj g) . t) <= x by A2, A5;

        

         A10: (g . x) in (g .: D) by A8, FUNCT_2: 35;

        

         A11: t <= (g . x) by A6, A9, WAYBEL_1: 8;

        (g . x) <= ( sup (g .: D)) by A10, YELLOW_2: 22;

        hence thesis by A11, ORDERS_2: 3;

      end;

      then (g . ( sup D)) <= ( sup (g .: D)) by A4, YELLOW_0: 32;

      hence thesis by A3, ORDERS_2: 2;

    end;

    definition

      let S,T be TopSpace;

      let f be Function of S, T;

      :: WAYBEL34:def9

      attr f is relatively_open means for V be open Subset of S holds (f .: V) is open Subset of (T | ( rng f));

    end

    theorem :: WAYBEL34:24

    for X,Y be non empty TopSpace holds for d be Function of X, Y holds d is relatively_open iff ( corestr d) is open

    proof

      let X,Y be non empty TopSpace;

      let d be Function of X, Y;

      

       A1: ( corestr d) = d by WAYBEL18:def 7;

      

       A2: ( Image d) = (Y | ( rng d)) by WAYBEL18:def 6;

      thus d is relatively_open implies ( corestr d) is open by A1, A2;

      assume

       A3: for V be Subset of X st V is open holds (( corestr d) .: V) is open;

      let V be open Subset of X;

      thus thesis by A1, A2, A3;

    end;

    theorem :: WAYBEL34:25

    

     Th25: for S,T be complete LATTICE, g be infs-preserving Function of S, T holds for X be Scott TopAugmentation of T holds for Y be Scott TopAugmentation of S holds for V be open Subset of X holds (( LowerAdj g) .: V) = (( rng ( LowerAdj g)) /\ ( uparrow (( LowerAdj g) .: V)))

    proof

      let S,T be complete LATTICE, g be infs-preserving Function of S, T;

      let X be Scott TopAugmentation of T;

      let Y be Scott TopAugmentation of S;

      

       A1: the RelStr of X = the RelStr of T by YELLOW_9:def 4;

      

       A2: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;

      then

      reconsider d = ( LowerAdj g) as Function of X, Y by A1;

      let V be open Subset of X;

      reconsider A = ( uparrow (( LowerAdj g) .: V)) as Subset of Y by A2;

      (d .: V) = (A /\ ( rng d))

      proof

        

         A3: (d .: V) c= A by WAYBEL_0: 16;

        (d .: V) c= ( rng d) by RELAT_1: 111;

        hence (d .: V) c= (A /\ ( rng d)) by A3, XBOOLE_1: 19;

        let t be object;

        assume

         A4: t in (A /\ ( rng d));

        then

         A5: t in A by XBOOLE_0:def 4;

        

         A6: t in ( rng d) by A4, XBOOLE_0:def 4;

        reconsider t as Element of S by A5;

        consider x be Element of S such that

         A7: x <= t and

         A8: x in (( LowerAdj g) .: V) by A5, WAYBEL_0:def 16;

        consider u be object such that

         A9: u in the carrier of T and

         A10: u in V and

         A11: x = (( LowerAdj g) . u) by A8, FUNCT_2: 64;

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

        then

        consider v be object such that

         A12: v in the carrier of T and

         A13: t = (d . v) by A6, FUNCT_1:def 3;

        reconsider u, v as Element of T by A9, A12;

        

         A14: (( LowerAdj g) . (u "\/" v)) = (x "\/" t) by A11, A13, WAYBEL_6: 2

        .= t by A7, YELLOW_0: 24;

        reconsider V9 = V as Subset of T by A1;

        V is upper by WAYBEL11:def 4;

        then

         A15: V9 is upper by A1, WAYBEL_0: 25;

        u <= (u "\/" v) by YELLOW_0: 22;

        then (u "\/" v) in V9 by A10, A15;

        hence thesis by A14, FUNCT_2: 35;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL34:26

    

     Th26: for S,T be complete LATTICE, g be infs-preserving Function of S, T holds for X be Scott TopAugmentation of T holds for Y be Scott TopAugmentation of S st for V be open Subset of X holds ( uparrow (( LowerAdj g) .: V)) is open Subset of Y holds for d be Function of X, Y st d = ( LowerAdj g) holds d is relatively_open

    proof

      let S,T be complete LATTICE, g be infs-preserving Function of S, T;

      let X be Scott TopAugmentation of T;

      let Y be Scott TopAugmentation of S such that

       A1: for V be open Subset of X holds ( uparrow (( LowerAdj g) .: V)) is open Subset of Y;

      let d be Function of X, Y such that

       A2: d = ( LowerAdj g);

      let V be open Subset of X;

      reconsider A = ( uparrow (( LowerAdj g) .: V)) as open Subset of Y by A1;

      (d .: V) = (A /\ ( rng d)) by A2, Th25;

      then

       A3: (d .: V) = (( [#] (Y | ( rng d))) /\ A) by PRE_TOPC:def 5;

      

       A4: A in the topology of Y by PRE_TOPC:def 2;

      reconsider B = (d .: V) as Subset of (Y | ( rng d)) by A3, XBOOLE_1: 17;

      B in the topology of (Y | ( rng d)) by A3, A4, PRE_TOPC:def 4;

      hence thesis by PRE_TOPC:def 2;

    end;

    registration

      let X,Y be complete LATTICE;

      let f be sups-preserving Function of X, Y;

      cluster ( Image f) -> complete;

      coherence by YELLOW_2: 34;

    end

    theorem :: WAYBEL34:27

    for S,T be complete LATTICE, g be infs-preserving Function of S, T holds for X be Scott TopAugmentation of T holds for Y be Scott TopAugmentation of S holds for Z be Scott TopAugmentation of ( Image ( LowerAdj g)) holds for d be Function of X, Y, d9 be Function of X, Z st d = ( LowerAdj g) & d9 = d holds d is relatively_open implies d9 is open

    proof

      let S,T be complete LATTICE, g be infs-preserving Function of S, T;

      let X be Scott TopAugmentation of T;

      let Y be Scott TopAugmentation of S;

      let Z be Scott TopAugmentation of ( Image ( LowerAdj g));

      let d be Function of X, Y, d9 be Function of X, Z such that

       A1: d = ( LowerAdj g) and

       A2: d9 = d and

       A3: for V be open Subset of X holds (d .: V) is open Subset of (Y | ( rng d));

      let V be Subset of X;

      assume V is open;

      then

      reconsider A = (d .: V) as open Subset of (Y | ( rng d)) by A3;

      

       A4: ( Image ( LowerAdj g)) = ( subrelstr ( rng ( LowerAdj g))) by YELLOW_2:def 2;

      then

       A5: the carrier of ( Image ( LowerAdj g)) = ( rng d) by A1, YELLOW_0:def 15;

      

       A6: ( [#] (Y | ( rng d))) = ( rng d) by PRE_TOPC:def 5;

      

       A7: the RelStr of Z = ( Image ( LowerAdj g)) by YELLOW_9:def 4;

      

       A8: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;

      reconsider B = A as Subset of Z by A1, A4, A6, A7, YELLOW_0:def 15;

      A in the topology of (Y | ( rng d)) by PRE_TOPC:def 2;

      then

      consider C be Subset of Y such that

       A9: C in the topology of Y and

       A10: A = (C /\ ( [#] (Y | ( rng d)))) by PRE_TOPC:def 4;

      C is open by A9;

      then

       A11: C is upper inaccessible by WAYBEL11:def 4;

      

       A12: B is upper

      proof

        let x,y be Element of Z;

        reconsider x9 = x, y9 = y as Element of ( Image ( LowerAdj g)) by A7;

        reconsider a = x9, b = y9 as Element of S by YELLOW_0: 58;

        reconsider a9 = a, b9 = b as Element of Y by A8;

        assume that

         A13: x in B and

         A14: x <= y;

        

         A15: x9 <= y9 by A7, A14, YELLOW_0: 1;

        

         A16: a in C by A10, A13, XBOOLE_0:def 4;

        a <= b by A15, YELLOW_0: 59;

        then a9 <= b9 by A8, YELLOW_0: 1;

        then b9 in C by A11, A16;

        hence thesis by A5, A6, A10, XBOOLE_0:def 4;

      end;

      B is inaccessible

      proof

        let D be directed non empty Subset of Z such that

         A17: ( sup D) in B;

        reconsider D9 = D as non empty Subset of ( Image ( LowerAdj g)) by A7;

        reconsider E = D9 as non empty Subset of S by A5, A8, XBOOLE_1: 1;

        reconsider E9 = E as non empty Subset of Y by A8;

        D9 is directed by A7, WAYBEL_0: 3;

        then E is directed by YELLOW_2: 7;

        then

         A18: E9 is directed by A8, WAYBEL_0: 3;

        

         A19: ex_sup_of (D9,S) by YELLOW_0: 17;

        ( Image ( LowerAdj g)) is sups-inheriting by YELLOW_2: 32;

        then ( "\/" (D9,S)) in the carrier of ( Image ( LowerAdj g)) by A19;

        

        then ( sup E) = ( sup D9) by YELLOW_0: 68

        .= ( sup D) by A7, YELLOW_0: 17, YELLOW_0: 26;

        then ( sup E9) = ( sup D) by A8, YELLOW_0: 17, YELLOW_0: 26;

        then ( sup E9) in C by A10, A17, XBOOLE_0:def 4;

        then C meets E by A11, A18;

        hence thesis by A5, A6, A10, XBOOLE_1: 77;

      end;

      hence thesis by A2, A12, WAYBEL11:def 4;

    end;

    theorem :: WAYBEL34:28

    

     Th28: for S,T be complete LATTICE, g be infs-preserving Function of S, T st g is one-to-one holds for X be Scott TopAugmentation of T holds for Y be Scott TopAugmentation of S holds for d be Function of X, Y st d = ( LowerAdj g) holds g is directed-sups-preserving iff d is open

    proof

      let S,T be complete LATTICE, g be infs-preserving Function of S, T such that

       A1: g is one-to-one;

      let X be Scott TopAugmentation of T;

      let Y be Scott TopAugmentation of S;

       [g, ( LowerAdj g)] is Galois by Def1;

      then ( LowerAdj g) is onto by A1, WAYBEL_1: 27;

      then

       A2: ( rng ( LowerAdj g)) = the carrier of S by FUNCT_2:def 3;

      

       A3: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;

      

       A4: the RelStr of X = the RelStr of T by YELLOW_9:def 4;

      

       A5: ( [#] Y) = the carrier of Y;

      let d be Function of X, Y such that

       A6: d = ( LowerAdj g);

      

       A7: (Y | ( rng d)) = the TopStruct of Y by A2, A3, A5, A6, TSEP_1: 93;

      thus g is directed-sups-preserving implies d is open

      proof

        assume g is directed-sups-preserving;

        then for V be open Subset of X holds ( uparrow (( LowerAdj g) .: V)) is open Subset of Y by Th21;

        then

         A8: d is relatively_open by A6, Th26;

        let V be Subset of X;

        assume V is open;

        then (d .: V) is open Subset of (Y | ( rng d)) by A8;

        hence (d .: V) in the topology of Y by A7, PRE_TOPC:def 2;

      end;

      assume

       A9: for V be Subset of X st V is open holds (d .: V) is open;

      now

        let X9 be Scott TopAugmentation of T;

        let Y9 be Scott TopAugmentation of S;

        let V9 be open Subset of X9;

        

         A10: the RelStr of X9 = the RelStr of T by YELLOW_9:def 4;

        

         A11: the RelStr of Y9 = the RelStr of S by YELLOW_9:def 4;

        reconsider V = V9 as Subset of X by A4, A10;

        reconsider V as open Subset of X by A4, A10, YELLOW_9: 50;

        reconsider d9 = d as Function of X9, Y9 by A3, A4, A10, A11;

        (d .: V) is open by A9;

        then

         A12: (d9 .: V9) is open Subset of Y9 by A3, A11, YELLOW_9: 50;

        then (d9 .: V9) is upper by WAYBEL11:def 4;

        then

         A13: ( uparrow (d9 .: V9)) c= (d9 .: V9) by WAYBEL_0: 24;

        (d9 .: V9) c= ( uparrow (d9 .: V9)) by WAYBEL_0: 16;

        then ( uparrow (d9 .: V9)) = (d9 .: V9) by A13;

        hence ( uparrow (( LowerAdj g) .: V9)) is open Subset of Y9 by A6, A11, A12, WAYBEL_0: 13;

      end;

      hence thesis by Th21;

    end;

    registration

      let X be complete LATTICE;

      let f be projection Function of X, X;

      cluster ( Image f) -> complete;

      coherence by WAYBEL_1: 54;

    end

    theorem :: WAYBEL34:29

    

     Th29: for L be complete LATTICE, k be kernel Function of L, L holds ( corestr k) is infs-preserving & ( inclusion k) is sups-preserving & ( LowerAdj ( corestr k)) = ( inclusion k) & ( UpperAdj ( inclusion k)) = ( corestr k)

    proof

      let L be complete LATTICE, k be kernel Function of L, L;

      

       A1: [( corestr k), ( inclusion k)] is Galois by WAYBEL_1: 39;

      then

       A2: ( inclusion k) is lower_adjoint;

      

       A3: ( corestr k) is upper_adjoint by A1;

      hence ( corestr k) is infs-preserving & ( inclusion k) is sups-preserving by A2;

      thus thesis by A1, A2, A3, Def1, Def2;

    end;

    theorem :: WAYBEL34:30

    

     Th30: for L be complete LATTICE, k be kernel Function of L, L holds k is directed-sups-preserving iff ( corestr k) is directed-sups-preserving

    proof

      let L be complete LATTICE, k be kernel Function of L, L;

      set ck = ( corestr k);

       [ck, ( inclusion k)] is Galois by WAYBEL_1: 39;

      then

       A1: ( inclusion k) is lower_adjoint;

      

       A2: k = (( inclusion k) * ck) by WAYBEL_1: 32;

      hereby

        assume

         A3: k is directed-sups-preserving;

        thus ( corestr k) is directed-sups-preserving

        proof

          let D be Subset of L;

          assume D is non empty directed;

          then

           A4: k preserves_sup_of D by A3;

          assume ex_sup_of (D,L);

          

          then

           A5: ( sup (k .: D)) = (k . ( sup D)) by A4

          .= (( inclusion k) . (ck . ( sup D))) by A2, FUNCT_2: 15

          .= (ck . ( sup D)) by FUNCT_1: 18;

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

          

           A6: ex_sup_of ((( inclusion k) .: (ck .: D)),L) by YELLOW_0: 17;

          

           A7: ( Image k) is sups-inheriting by WAYBEL_1: 53;

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

          then

           A8: ( "\/" ((ck .: D),L)) in the carrier of ( Image k) by A7;

          (ck .: D) = (( inclusion k) .: (ck .: D)) by WAYBEL15: 12;

          

          hence ( sup (ck .: D)) = ( sup (( inclusion k) .: (ck .: D))) by A6, A8, YELLOW_0: 64

          .= (ck . ( sup D)) by A2, A5, RELAT_1: 126;

        end;

      end;

      thus thesis by A1, A2, WAYBEL15: 11;

    end;

    theorem :: WAYBEL34:31

    for L be complete LATTICE, k be kernel Function of L, L holds k is directed-sups-preserving iff for X be Scott TopAugmentation of ( Image k) holds for Y be Scott TopAugmentation of L holds for V be Subset of L st V is open Subset of X holds ( uparrow V) is open Subset of Y

    proof

      let L be complete LATTICE, k be kernel Function of L, L;

      

       A1: [( corestr k), ( inclusion k)] is Galois by WAYBEL_1: 39;

      then

       A2: ( corestr k) is upper_adjoint;

      then

       A3: ( inclusion k) = ( LowerAdj ( corestr k)) by A1, Def1;

      hereby

        assume

         A4: k is directed-sups-preserving;

        let X be Scott TopAugmentation of ( Image k);

        let Y be Scott TopAugmentation of L;

        

         A5: the RelStr of X = ( Image k) by YELLOW_9:def 4;

        let V be Subset of L;

        assume V is open Subset of X;

        then

        reconsider A = V as open Subset of X;

        reconsider B = A as Subset of ( Image k) by A5;

        

         A6: ( corestr k) is directed-sups-preserving by A4, Th30;

        (( inclusion k) .: B) = V by WAYBEL15: 12;

        hence ( uparrow V) is open Subset of Y by A2, A3, A6, Th21;

      end;

      assume

       A7: for X be Scott TopAugmentation of ( Image k) holds for Y be Scott TopAugmentation of L holds for V be Subset of L st V is open Subset of X holds ( uparrow V) is open Subset of Y;

      now

        set g = ( corestr k);

        let X be Scott TopAugmentation of ( Image k);

        let Y be Scott TopAugmentation of L;

        let V be open Subset of X;

         the RelStr of X = ( Image k) by YELLOW_9:def 4;

        then

        reconsider B = V as Subset of ( Image k);

        the carrier of ( Image k) c= the carrier of L by YELLOW_0:def 13;

        then

        reconsider A = B as Subset of L by XBOOLE_1: 1;

        ( uparrow A) is open Subset of Y by A7;

        hence ( uparrow (( LowerAdj g) .: V)) is open Subset of Y by A3, WAYBEL15: 12;

      end;

      then ( corestr k) is directed-sups-preserving by A2, Th21;

      hence thesis by Th30;

    end;

    theorem :: WAYBEL34:32

    

     Th32: for L be complete LATTICE holds for S be sups-inheriting non empty full SubRelStr of L holds for x,y be Element of L, a,b be Element of S st a = x & b = y holds x << y implies a << b

    proof

      let L be complete LATTICE;

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

      let x,y be Element of L, a,b be Element of S such that

       A1: a = x and

       A2: b = y and

       A3: for D be non empty directed Subset of L st y <= ( sup D) holds ex d be Element of L st d in D & x <= d;

      let D be non empty directed Subset of S such that

       A4: b <= ( sup D);

      reconsider E = D as non empty directed Subset of L by YELLOW_2: 7;

      

       A5: ex_sup_of (D,L) by YELLOW_0: 17;

      then ( "\/" (D,L)) in the carrier of S by YELLOW_0:def 19;

      then ( sup E) = ( sup D) by A5, YELLOW_0: 64;

      then y <= ( sup E) by A2, A4, YELLOW_0: 59;

      then

      consider e be Element of L such that

       A6: e in E and

       A7: x <= e by A3;

      reconsider d = e as Element of S by A6;

      take d;

      thus thesis by A1, A6, A7, YELLOW_0: 60;

    end;

    theorem :: WAYBEL34:33

    for L be complete LATTICE, k be kernel Function of L, L st k is directed-sups-preserving holds for x,y be Element of L, a,b be Element of ( Image k) st a = x & b = y holds x << y iff a << b

    proof

      let L be complete LATTICE, k be kernel Function of L, L;

      set g = ( corestr k);

      assume k is directed-sups-preserving;

      then ( corestr k) is directed-sups-preserving infs-preserving by Th29, Th30;

      then

       A1: ( LowerAdj g) is waybelow-preserving by Th22;

      let x,y be Element of L, a,b be Element of ( Image k);

      

       A2: ( Image k) is sups-inheriting by WAYBEL_1: 53;

      

       A3: ( inclusion k) = ( LowerAdj g) by Th29;

      then

       A4: (( LowerAdj g) . a) = a by FUNCT_1: 18;

      (( LowerAdj g) . b) = b by A3, FUNCT_1: 18;

      hence thesis by A1, A2, A4, Th32;

    end;

    theorem :: WAYBEL34:34

    for L be complete LATTICE, k be kernel Function of L, L st ( Image k) is continuous & for x,y be Element of L, a,b be Element of ( Image k) st a = x & b = y holds x << y iff a << b holds k is directed-sups-preserving

    proof

      let L be complete LATTICE, k be kernel Function of L, L such that

       A1: ( Image k) is continuous and

       A2: for x,y be Element of L, a,b be Element of ( Image k) st a = x & b = y holds x << y iff a << b;

      set g = ( corestr k);

      

       A3: ( corestr k) is infs-preserving by Th29;

      ( LowerAdj g) is waybelow-preserving

      proof

        let t,t9 be Element of ( Image k);

        

         A4: ( LowerAdj g) = ( inclusion k) by Th29;

        then

         A5: (( LowerAdj g) . t) = t by FUNCT_1: 18;

        (( LowerAdj g) . t9) = t9 by A4, FUNCT_1: 18;

        hence thesis by A2, A5;

      end;

      then ( corestr k) is directed-sups-preserving by A1, A3, Th23;

      hence thesis by Th30;

    end;

    theorem :: WAYBEL34:35

    

     Th35: for L be complete LATTICE, c be closure Function of L, L holds ( corestr c) is sups-preserving & ( inclusion c) is infs-preserving & ( UpperAdj ( corestr c)) = ( inclusion c) & ( LowerAdj ( inclusion c)) = ( corestr c)

    proof

      let L be complete LATTICE, c be closure Function of L, L;

      

       A1: [( inclusion c), ( corestr c)] is Galois by WAYBEL_1: 36;

      then

       A2: ( inclusion c) is upper_adjoint;

      

       A3: ( corestr c) is lower_adjoint by A1;

      hence ( corestr c) is sups-preserving & ( inclusion c) is infs-preserving by A2;

      thus thesis by A1, A2, A3, Def1, Def2;

    end;

    theorem :: WAYBEL34:36

    

     Th36: for L be complete LATTICE, c be closure Function of L, L holds ( Image c) is directed-sups-inheriting iff ( inclusion c) is directed-sups-preserving

    proof

      let L be complete LATTICE, c be closure Function of L, L;

      set ic = ( inclusion c);

      thus ( Image c) is directed-sups-inheriting implies ( inclusion c) is directed-sups-preserving

      proof

        assume

         A1: ( Image c) is directed-sups-inheriting;

        let D be Subset of ( Image c);

        assume

         A2: D is non empty directed;

        then

        reconsider E = D as non empty directed Subset of L by YELLOW_2: 7;

        

         A3: (ic .: D) = E by WAYBEL15: 12;

        assume ex_sup_of (D,( Image c));

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

        

        hence ( sup (ic .: D)) = ( sup D) by A1, A2, A3, WAYBEL_0: 7

        .= (ic . ( sup D)) by FUNCT_1: 18;

      end;

      assume

       A4: ( inclusion c) is directed-sups-preserving;

      let X be directed Subset of ( Image c);

      assume

       A5: X <> {} ;

      assume ex_sup_of (X,L);

      

       A6: ic preserves_sup_of X by A4, A5;

       ex_sup_of (X,( Image c)) by YELLOW_0: 17;

      

      then ( sup (ic .: X)) = (ic . ( sup X)) by A6

      .= ( sup X) by FUNCT_1: 18;

      then ( sup (ic .: X)) in the carrier of ( Image c);

      hence thesis by WAYBEL15: 12;

    end;

    theorem :: WAYBEL34:37

    for L be complete LATTICE, c be closure Function of L, L holds ( Image c) is directed-sups-inheriting iff for X be Scott TopAugmentation of ( Image c) holds for Y be Scott TopAugmentation of L holds for f be Function of Y, X st f = c holds f is open

    proof

      let L be complete LATTICE, c be closure Function of L, L;

      

       A1: ( LowerAdj ( inclusion c)) = ( corestr c) by Th35;

      

       A2: ( corestr c) = c by WAYBEL_1: 30;

      

       A3: ( inclusion c) is infs-preserving Function of ( Image c), L by Th35;

      

       A4: ( Image c) is directed-sups-inheriting iff ( inclusion c) is directed-sups-preserving by Th36;

      hence ( Image c) is directed-sups-inheriting implies for X be Scott TopAugmentation of ( Image c) holds for Y be Scott TopAugmentation of L holds for f be Function of Y, X st f = c holds f is open by A1, A2, A3, Th28;

      assume

       A5: for X be Scott TopAugmentation of ( Image c) holds for Y be Scott TopAugmentation of L holds for f be Function of Y, X st f = c holds f is open;

      set X = the Scott TopAugmentation of ( Image c), Y = the Scott TopAugmentation of L;

      

       A6: the RelStr of X = the RelStr of ( Image c) by YELLOW_9:def 4;

       the RelStr of Y = the RelStr of L by YELLOW_9:def 4;

      then

      reconsider f = c as Function of Y, X by A2, A6;

      f is open by A5;

      hence thesis by A1, A2, A3, A4, Th28;

    end;

    theorem :: WAYBEL34:38

    for L be complete LATTICE, c be closure Function of L, L holds ( Image c) is directed-sups-inheriting implies ( corestr c) is waybelow-preserving

    proof

      let L be complete LATTICE, c be closure Function of L, L;

      assume ( Image c) is directed-sups-inheriting;

      then ( inclusion c) is directed-sups-preserving infs-preserving by Th35, Th36;

      then ( LowerAdj ( inclusion c)) is waybelow-preserving by Th22;

      hence thesis by Th35;

    end;

    theorem :: WAYBEL34:39

    for L be continuous complete LATTICE, c be closure Function of L, L st ( corestr c) is waybelow-preserving holds ( Image c) is directed-sups-inheriting

    proof

      let L be continuous complete LATTICE, c be closure Function of L, L;

      assume

       A1: ( corestr c) is waybelow-preserving;

      

       A2: ( LowerAdj ( inclusion c)) = ( corestr c) by Th35;

      ( inclusion c) is infs-preserving by Th35;

      then ( inclusion c) is directed-sups-preserving by A1, A2, Th23;

      hence thesis by Th36;

    end;

    begin

    definition

      let W be non empty set;

      set A = (W -INF_category );

      defpred P[ set] means not contradiction;

      defpred Q[ Object of A, Object of A, Morphism of $1, $2] means ( @ $3) is directed-sups-preserving;

      

       A1: ex a be Object of A st P[a];

      

       A2: for a,b,c be Object of A st P[a] & P[b] & P[c] & <^a, b^> <> {} & <^b, c^> <> {} holds for f be Morphism of a, b, g be Morphism of b, c st Q[a, b, f] & Q[b, c, g] holds Q[a, c, (g * f)]

      proof

        let a,b,c be Object of A such that

         A3: <^a, b^> <> {} and

         A4: <^b, c^> <> {} ;

        let f be Morphism of a, b, g be Morphism of b, c;

        

         A5: <^a, c^> <> {} by A3, A4, ALTCAT_1:def 2;

        

         A6: ( @ f) = f by A3, YELLOW21:def 7;

        

         A7: ( @ g) = g by A4, YELLOW21:def 7;

        ( @ (g * f)) = (g * f) by A5, YELLOW21:def 7;

        then ( @ (g * f)) = (( @ g) * ( @ f)) by A3, A4, A5, A6, A7, ALTCAT_1:def 12;

        hence thesis by WAYBEL20: 28;

      end;

      

       A8: for a be Object of A st P[a] holds Q[a, a, ( idm a)]

      proof

        let a be Object of A;

        ( idm a) = ( id ( latt a)) by YELLOW21: 2;

        hence thesis by YELLOW21:def 7;

      end;

      :: WAYBEL34:def10

      func W -INF(SC)_category -> strict non empty subcategory of (W -INF_category ) means

      : Def10: (for a be Object of (W -INF_category ) holds a is Object of it ) & for a,b be Object of (W -INF_category ) holds for a9,b9 be Object of it st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff ( @ f) is directed-sups-preserving;

      existence

      proof

        ex B be strict non empty subcategory of A st (for a be Object of A holds a is Object of B iff P[a]) & for a,b be Object of A, a9,b9 be Object of B st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f] from YELLOW18:sch 7( A1, A2, A8);

        hence thesis;

      end;

      correctness

      proof

        let B1,B2 be strict non empty subcategory of A;

        assume for a be Object of (W -INF_category ) holds a is Object of B1;

        then

         A9: for a be Object of (W -INF_category ) holds a is Object of B1 iff P[a];

        assume

         A10: for a,b be Object of (W -INF_category ) holds for a9,b9 be Object of B1 st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f];

        assume for a be Object of (W -INF_category ) holds a is Object of B2;

        then

         A11: for a be Object of (W -INF_category ) holds a is Object of B2 iff P[a];

        assume

         A12: for a,b be Object of (W -INF_category ) holds for a9,b9 be Object of B2 st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f];

         the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 1( A9, A10, A11, A12);

        hence thesis;

      end;

    end

    definition

      let W be with_non-empty_element set;

      

       A1: ex w be non empty set st w in W by SETFAM_1:def 10;

      set A = (W -SUP_category );

      defpred P[ set] means not contradiction;

      defpred Q[ Object of A, Object of A, Morphism of $1, $2] means ( UpperAdj ( @ $3)) is directed-sups-preserving;

      

       A2: ex a be Object of A st P[a];

      

       A3: for a,b,c be Object of A st P[a] & P[b] & P[c] & <^a, b^> <> {} & <^b, c^> <> {} holds for f be Morphism of a, b, g be Morphism of b, c st Q[a, b, f] & Q[b, c, g] holds Q[a, c, (g * f)]

      proof

        let a,b,c be Object of A such that

         A4: <^a, b^> <> {} and

         A5: <^b, c^> <> {} ;

        let f be Morphism of a, b, g be Morphism of b, c;

        

         A6: <^a, c^> <> {} by A4, A5, ALTCAT_1:def 2;

        

         A7: ( @ f) = f by A4, YELLOW21:def 7;

        

         A8: ( @ g) = g by A5, YELLOW21:def 7;

        

         A9: ( @ (g * f)) = (g * f) by A6, YELLOW21:def 7;

        

         A10: ( @ g) is sups-preserving Function of ( latt b), ( latt c) by A1, A5, A8, Def5;

        

         A11: ( @ f) is sups-preserving Function of ( latt a), ( latt b) by A1, A4, A7, Def5;

        ( @ (g * f)) = (( @ g) * ( @ f)) by A4, A5, A6, A7, A8, A9, ALTCAT_1:def 12;

        then ( UpperAdj ( @ (g * f))) = (( UpperAdj ( @ f)) * ( UpperAdj ( @ g))) by A10, A11, Th9;

        hence thesis by WAYBEL20: 28;

      end;

      

       A12: for a be Object of A st P[a] holds Q[a, a, ( idm a)]

      proof

        let a be Object of A;

        

         A13: ( idm a) = ( id ( latt a)) by YELLOW21: 2;

        ( UpperAdj ( id ( latt a))) = ( id ( latt a)) by Th7;

        hence thesis by A13, YELLOW21:def 7;

      end;

      :: WAYBEL34:def11

      func W -SUP(SO)_category -> strict non empty subcategory of (W -SUP_category ) means

      : Def11: (for a be Object of (W -SUP_category ) holds a is Object of it ) & for a,b be Object of (W -SUP_category ) holds for a9,b9 be Object of it st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff ( UpperAdj ( @ f)) is directed-sups-preserving;

      existence

      proof

        ex B be strict non empty subcategory of A st (for a be Object of A holds a is Object of B iff P[a]) & for a,b be Object of A, a9,b9 be Object of B st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f] from YELLOW18:sch 7( A2, A3, A12);

        hence thesis;

      end;

      correctness

      proof

        let B1,B2 be strict non empty subcategory of A;

        assume for a be Object of (W -SUP_category ) holds a is Object of B1;

        then

         A14: for a be Object of (W -SUP_category ) holds a is Object of B1 iff P[a];

        assume

         A15: for a,b be Object of (W -SUP_category ) holds for a9,b9 be Object of B1 st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f];

        assume for a be Object of (W -SUP_category ) holds a is Object of B2;

        then

         A16: for a be Object of (W -SUP_category ) holds a is Object of B2 iff P[a];

        assume

         A17: for a,b be Object of (W -SUP_category ) holds for a9,b9 be Object of B2 st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f];

         the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 1( A14, A15, A16, A17);

        hence thesis;

      end;

    end

    theorem :: WAYBEL34:40

    

     Th40: for S be non empty RelStr, T be non empty reflexive antisymmetric RelStr holds for t be Element of T holds for X be non empty Subset of S holds (S --> t) preserves_sup_of X & (S --> t) preserves_inf_of X

    proof

      let S be non empty RelStr;

      let T be non empty reflexive antisymmetric RelStr;

      let t be Element of T;

      let X be non empty Subset of S;

      set f = (S --> t);

      

       A1: (f .: X) = {t}

      proof

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

        set x = the Element of X;

        (f . x) = t by FUNCOP_1: 7;

        then t in (f .: X) by FUNCT_2: 35;

        hence thesis by ZFMISC_1: 31;

      end;

      

       A2: (f . ( sup X)) = t by FUNCOP_1: 7;

      

       A3: (f . ( inf X)) = t by FUNCOP_1: 7;

      

       A4: ( inf {t}) = t by YELLOW_0: 39;

      

       A5: ( sup {t}) = t by YELLOW_0: 39;

      

       A6: ex_sup_of ( {t},T) by YELLOW_0: 38;

       ex_inf_of ( {t},T) by YELLOW_0: 38;

      hence thesis by A1, A2, A3, A4, A5, A6;

    end;

    theorem :: WAYBEL34:41

    

     Th41: for S be non empty RelStr holds for T be lower-bounded non empty reflexive antisymmetric RelStr holds (S --> ( Bottom T)) is sups-preserving

    proof

      let S be non empty RelStr;

      let T be lower-bounded non empty reflexive antisymmetric RelStr;

      let X be Subset of S such that ex_sup_of (X,S);

      set f = (the carrier of S --> ( Bottom T));

      

       A1: (f . ( sup X)) = ( Bottom T) by FUNCOP_1: 7;

      ((S --> ( Bottom T)) .: X) c= {( Bottom T)} by FUNCOP_1: 81;

      then ((S --> ( Bottom T)) .: X) = {( Bottom T)} or ((S --> ( Bottom T)) .: X) = {} by ZFMISC_1: 33;

      hence thesis by A1, YELLOW_0: 38, YELLOW_0: 39, YELLOW_0: 42;

    end;

    theorem :: WAYBEL34:42

    

     Th42: for S be non empty RelStr holds for T be upper-bounded non empty reflexive antisymmetric RelStr holds (S --> ( Top T)) is infs-preserving

    proof

      let S be non empty RelStr;

      let T be upper-bounded non empty reflexive antisymmetric RelStr;

      let X be Subset of S such that ex_inf_of (X,S);

      set t = ( Top T), f = (the carrier of S --> t);

      

       A1: (f . ( inf X)) = t by FUNCOP_1: 7;

      ((S --> t) .: X) c= {t} by FUNCOP_1: 81;

      then ((S --> t) .: X) = {t} or ((S --> t) .: X) = {} by ZFMISC_1: 33;

      hence thesis by A1, YELLOW_0: 38, YELLOW_0: 39, YELLOW_0: 43;

    end;

    registration

      let S be non empty RelStr;

      let T be upper-bounded non empty reflexive antisymmetric RelStr;

      cluster (S --> ( Top T)) -> directed-sups-preserving infs-preserving;

      coherence by Th40, Th42;

    end

    registration

      let S be non empty RelStr;

      let T be lower-bounded non empty reflexive antisymmetric RelStr;

      cluster (S --> ( Bottom T)) -> filtered-infs-preserving sups-preserving;

      coherence by Th40, Th41;

    end

    registration

      let S be non empty RelStr;

      let T be upper-bounded non empty reflexive antisymmetric RelStr;

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

      existence

      proof

        take (S --> ( Top T));

        thus thesis;

      end;

    end

    registration

      let S be non empty RelStr;

      let T be lower-bounded non empty reflexive antisymmetric RelStr;

      cluster filtered-infs-preserving sups-preserving for Function of S, T;

      existence

      proof

        take (S --> ( Bottom T));

        thus thesis;

      end;

    end

    theorem :: WAYBEL34:43

    

     Th43: for W be with_non-empty_element set holds for L be LATTICE holds L is Object of (W -INF(SC)_category ) iff L is strict complete & the carrier of L in W

    proof

      let W be with_non-empty_element set;

      let L be LATTICE;

      the carrier of (W -INF(SC)_category ) c= the carrier of (W -INF_category ) by ALTCAT_2:def 11;

      then L in the carrier of (W -INF(SC)_category ) implies L is Object of (W -INF_category );

      then L is Object of (W -INF(SC)_category ) iff L is Object of (W -INF_category ) by Def10;

      hence thesis by Th13;

    end;

    theorem :: WAYBEL34:44

    

     Th44: for W be with_non-empty_element set holds for a,b be Object of (W -INF(SC)_category ) holds for f be set holds f in <^a, b^> iff f is directed-sups-preserving infs-preserving Function of ( latt a), ( latt b)

    proof

      let W be with_non-empty_element set;

      let a,b be Object of (W -INF(SC)_category ), f be set;

      the carrier of (W -INF(SC)_category ) c= the carrier of (W -INF_category ) by ALTCAT_2:def 11;

      then

      reconsider a1 = a, b1 = b as Object of (W -INF_category );

      hereby

        assume

         A1: f in <^a, b^>;

        

         A2: <^a, b^> c= <^a1, b1^> by ALTCAT_2: 31;

        then

        reconsider g = f as Morphism of a1, b1 by A1;

        f = ( @ g) by A1, A2, YELLOW21:def 7;

        hence f is directed-sups-preserving infs-preserving Function of ( latt a), ( latt b) by A1, A2, Def10, Th14;

      end;

      assume f is directed-sups-preserving infs-preserving Function of ( latt a), ( latt b);

      then

      reconsider f as directed-sups-preserving infs-preserving Function of ( latt a), ( latt b);

      

       A3: f in <^a1, b1^> by Th14;

      reconsider g = f as Morphism of a1, b1 by Th14;

      f = ( @ g) by A3, YELLOW21:def 7;

      hence thesis by A3, Def10;

    end;

    theorem :: WAYBEL34:45

    for W be with_non-empty_element set holds for L be LATTICE holds L is Object of (W -SUP(SO)_category ) iff L is strict complete & the carrier of L in W

    proof

      let W be with_non-empty_element set;

      let L be LATTICE;

      the carrier of (W -SUP(SO)_category ) c= the carrier of (W -SUP_category ) by ALTCAT_2:def 11;

      then L in the carrier of (W -SUP(SO)_category ) implies L is Object of (W -SUP_category );

      then L is Object of (W -SUP(SO)_category ) iff L is Object of (W -SUP_category ) by Def11;

      hence thesis by Th15;

    end;

    theorem :: WAYBEL34:46

    

     Th46: for W be with_non-empty_element set holds for a,b be Object of (W -SUP(SO)_category ) holds for f be set holds f in <^a, b^> iff ex g be sups-preserving Function of ( latt a), ( latt b) st g = f & ( UpperAdj g) is directed-sups-preserving

    proof

      let W be with_non-empty_element set;

      let a,b be Object of (W -SUP(SO)_category ), f be set;

      the carrier of (W -SUP(SO)_category ) c= the carrier of (W -SUP_category ) by ALTCAT_2:def 11;

      then

      reconsider a1 = a, b1 = b as Object of (W -SUP_category );

      hereby

        assume

         A1: f in <^a, b^>;

        

         A2: <^a, b^> c= <^a1, b1^> by ALTCAT_2: 31;

        then

        reconsider g = f as Morphism of a1, b1 by A1;

        

         A3: f = ( @ g) by A1, A2, YELLOW21:def 7;

        

         A4: ( UpperAdj ( @ g)) is directed-sups-preserving by A1, A2, Def11;

        f is sups-preserving Function of ( latt a1), ( latt b1) by A1, A2, Th16;

        hence ex g be sups-preserving Function of ( latt a), ( latt b) st g = f & ( UpperAdj g) is directed-sups-preserving by A3, A4;

      end;

      given g be sups-preserving Function of ( latt a), ( latt b) such that

       A5: g = f and

       A6: ( UpperAdj g) is directed-sups-preserving;

      

       A7: f in <^a1, b1^> by A5, Th16;

      reconsider g = f as Morphism of a1, b1 by A5, Th16;

      f = ( @ g) by A7, YELLOW21:def 7;

      hence thesis by A5, A6, A7, Def11;

    end;

    theorem :: WAYBEL34:47

    for W be with_non-empty_element set holds (W -INF(SC)_category ) = ( Intersect ((W -INF_category ),(W -UPS_category )))

    proof

      let W be with_non-empty_element set;

      consider w be non empty set such that

       A1: w in W by SETFAM_1:def 10;

      set r = the upper-bounded well-ordering Order of w;

       A2:

      now

        let a be Object of (W -INF_category ), b be Object of (W -UPS_category );

        ( idm a) = ( id ( latt a)) by YELLOW21: 2;

        hence a = b implies ( idm a) = ( idm b) by YELLOW21: 2;

      end;

      set B = ( Intersect ((W -INF_category ),(W -UPS_category )));

      

       A3: ((W -INF_category ),(W -UPS_category )) have_the_same_composition by YELLOW20: 12;

      then

       A4: the carrier of B = (the carrier of (W -INF_category ) /\ the carrier of (W -UPS_category )) by YELLOW20:def 3;

      

       A5: RelStr (# w, r #) is Object of (W -INF_category ) by A1, Th13;

       RelStr (# w, r #) is Object of (W -UPS_category ) by A1, YELLOW21: 14;

      then ( Intersect ((W -INF_category ),(W -UPS_category ))) is non empty by A4, A5, XBOOLE_0:def 4;

      then

      reconsider I = ( Intersect ((W -INF_category ),(W -UPS_category ))) as non empty subcategory of (W -INF_category ) by A2, YELLOW20: 12, YELLOW20: 25;

      set A = (W -INF(SC)_category );

      deffunc B( set, set) = (the Arrows of A . ($1,$2));

      

       A6: for C1,C2 be para-functional semi-functional category st the carrier of C1 = the carrier of A & (for a,b be Object of C1 holds <^a, b^> = B(a,b)) & the carrier of C2 = the carrier of A & (for a,b be Object of C2 holds <^a, b^> = B(a,b)) holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW18:sch 19;

      

       A7: the carrier of I = the carrier of A

      proof

        thus the carrier of I c= the carrier of A

        proof

          let x be object;

          assume x in the carrier of I;

          then

          reconsider x as Object of I;

          reconsider L = x as LATTICE by YELLOW21:def 4;

          

           A8: x in the carrier of (W -UPS_category ) by A4, XBOOLE_0:def 4;

          then

           A9: L is strict complete by A1, YELLOW21:def 10;

          the carrier of L in W by A1, A8, YELLOW21:def 10;

          then L is Object of A by A9, Th43;

          hence thesis;

        end;

        let x be object;

        assume x in the carrier of A;

        then

        reconsider x as Object of A;

        reconsider L = x as LATTICE by YELLOW21:def 4;

        

         A10: L is complete strict by Th43;

        

         A11: the carrier of L in W by Th43;

        then

         A12: x is Object of (W -INF_category ) by A10, Th13;

        x is Object of (W -UPS_category ) by A10, A11, YELLOW21:def 10;

        hence thesis by A4, A12, XBOOLE_0:def 4;

      end;

      

       A13: for a,b be Object of A holds <^a, b^> = B(a,b) by ALTCAT_1:def 1;

      now

        let a,b be Object of I;

        reconsider a9 = a, b9 = b as Object of A by A7;

        reconsider a1 = a, b1 = b as Object of (W -INF_category ) by A4, XBOOLE_0:def 4;

        reconsider a2 = a, b2 = b as Object of (W -UPS_category ) by A4, XBOOLE_0:def 4;

        

         A14: ( dom the Arrows of (W -INF_category )) = [:the carrier of (W -INF_category ), the carrier of (W -INF_category ):] by PARTFUN1:def 2;

        ( dom the Arrows of (W -UPS_category )) = [:the carrier of (W -UPS_category ), the carrier of (W -UPS_category ):] by PARTFUN1:def 2;

        then

         A15: (( dom the Arrows of (W -INF_category )) /\ ( dom the Arrows of (W -UPS_category ))) = [:(the carrier of (W -INF_category ) /\ the carrier of (W -UPS_category )), (the carrier of (W -INF_category ) /\ the carrier of (W -UPS_category )):] by A14, ZFMISC_1: 100;

        

         A16: <^a, b^> = (the Arrows of I . (a,b)) by ALTCAT_1:def 1

        .= (( Intersect (the Arrows of (W -INF_category ),the Arrows of (W -UPS_category ))) . [a, b]) by A3, YELLOW20:def 3

        .= ((the Arrows of (W -INF_category ) . (a,b)) /\ (the Arrows of (W -UPS_category ) . [a, b])) by A4, A15, YELLOW20:def 2

        .= ( <^a1, b1^> /\ (the Arrows of (W -UPS_category ) . (a,b))) by ALTCAT_1:def 1

        .= ( <^a1, b1^> /\ <^a2, b2^>) by ALTCAT_1:def 1;

        now

          let f be object;

          f in <^a, b^> iff f in <^a1, b1^> & f in <^a2, b2^> by A16, XBOOLE_0:def 4;

          then f in <^a, b^> iff f is directed-sups-preserving Function of ( latt a2), ( latt b2) & f is infs-preserving Function of ( latt a1), ( latt b1) by Th14, YELLOW21: 15;

          then f in <^a, b^> iff f in <^a9, b9^> by Th44;

          hence f in <^a, b^> iff f in B(a,b) by ALTCAT_1:def 1;

        end;

        hence <^a, b^> = B(a,b) by TARSKI: 2;

      end;

      hence thesis by A6, A7, A13;

    end;

    definition

      let W be with_non-empty_element set;

      defpred P[ Object of (W -INF(SC)_category )] means ( latt $1) is continuous;

      consider a be non empty set such that

       A1: a in W by SETFAM_1:def 10;

      set r = the upper-bounded well-ordering Order of a;

      set b = RelStr (# a, r #);

      :: WAYBEL34:def12

      func W -CL_category -> strict full non empty subcategory of (W -INF(SC)_category ) means

      : Def12: for a be Object of (W -INF(SC)_category ) holds a is Object of it iff ( latt a) is continuous;

      existence

      proof

        b is Object of (W -INF_category ) by A1, Def4;

        then

        reconsider b as Object of (W -INF(SC)_category ) by Def10;

        b = ( latt b);

        then

         A2: ex b be Object of (W -INF(SC)_category ) st P[b];

        thus ex B be strict full non empty subcategory of (W -INF(SC)_category ) st for a be Object of (W -INF(SC)_category ) holds a is Object of B iff P[a] from YELLOW20:sch 2( A2);

      end;

      correctness

      proof

        let B1,B2 be strict full non empty subcategory of (W -INF(SC)_category ) such that

         A3: for a be Object of (W -INF(SC)_category ) holds a is Object of B1 iff P[a] and

         A4: for a be Object of (W -INF(SC)_category ) holds a is Object of B2 iff P[a];

         the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 3( A3, A4);

        hence thesis;

      end;

    end

    registration

      let W be with_non-empty_element set;

      cluster (W -CL_category ) -> with_complete_lattices;

      coherence ;

    end

    theorem :: WAYBEL34:48

    

     Th48: for W be with_non-empty_element set holds for L be LATTICE st the carrier of L in W holds L is Object of (W -CL_category ) iff L is strict complete continuous

    proof

      let W be with_non-empty_element set;

      

       A1: ex a be non empty set st a in W by SETFAM_1:def 10;

      

       A2: the carrier of (W -INF(SC)_category ) c= the carrier of (W -INF_category ) by ALTCAT_2:def 11;

      

       A3: the carrier of (W -CL_category ) c= the carrier of (W -INF(SC)_category ) by ALTCAT_2:def 11;

      let L be LATTICE;

      assume

       A4: the carrier of L in W;

      hereby

        assume

         A5: L is Object of (W -CL_category );

        then L in the carrier of (W -CL_category );

        then

        reconsider a = L as Object of (W -INF(SC)_category ) by A3;

        

         A6: a in the carrier of (W -INF(SC)_category );

        ( latt a) is continuous by A5, Def12;

        hence L is strict complete continuous by A1, A2, A6, Def4;

      end;

      assume

       A7: L is strict complete continuous;

      then L is Object of (W -INF_category ) by A4, Def4;

      then

      reconsider a = L as Object of (W -INF(SC)_category ) by Def10;

      ( latt a) = L;

      hence thesis by A7, Def12;

    end;

    theorem :: WAYBEL34:49

    

     Th49: for W be with_non-empty_element set holds for a,b be Object of (W -CL_category ) holds for f be set holds f in <^a, b^> iff f is infs-preserving directed-sups-preserving Function of ( latt a), ( latt b)

    proof

      let W be with_non-empty_element set;

      let a,b be Object of (W -CL_category ), f be set;

      the carrier of (W -CL_category ) c= the carrier of (W -INF(SC)_category ) by ALTCAT_2:def 11;

      then

      reconsider a1 = a, b1 = b as Object of (W -INF(SC)_category );

       <^a, b^> = <^a1, b1^> by ALTCAT_2: 28;

      hence thesis by Th44;

    end;

    definition

      let W be with_non-empty_element set;

      defpred P[ Object of (W -SUP(SO)_category )] means ( latt $1) is continuous;

      consider a be non empty set such that

       A1: a in W by SETFAM_1:def 10;

      set r = the upper-bounded well-ordering Order of a;

      set b = RelStr (# a, r #);

      :: WAYBEL34:def13

      func W -CL-opp_category -> strict full non empty subcategory of (W -SUP(SO)_category ) means

      : Def13: for a be Object of (W -SUP(SO)_category ) holds a is Object of it iff ( latt a) is continuous;

      existence

      proof

        b is Object of (W -SUP_category ) by A1, Def5;

        then

        reconsider b as Object of (W -SUP(SO)_category ) by Def11;

        b = ( latt b);

        then

         A2: ex b be Object of (W -SUP(SO)_category ) st P[b];

        thus ex B be strict full non empty subcategory of (W -SUP(SO)_category ) st for a be Object of (W -SUP(SO)_category ) holds a is Object of B iff P[a] from YELLOW20:sch 2( A2);

      end;

      correctness

      proof

        let B1,B2 be strict full non empty subcategory of (W -SUP(SO)_category ) such that

         A3: for a be Object of (W -SUP(SO)_category ) holds a is Object of B1 iff P[a] and

         A4: for a be Object of (W -SUP(SO)_category ) holds a is Object of B2 iff P[a];

         the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 3( A3, A4);

        hence thesis;

      end;

    end

    theorem :: WAYBEL34:50

    

     Th50: for W be with_non-empty_element set holds for L be LATTICE st the carrier of L in W holds L is Object of (W -CL-opp_category ) iff L is strict complete continuous

    proof

      let W be with_non-empty_element set;

      

       A1: ex a be non empty set st a in W by SETFAM_1:def 10;

      

       A2: the carrier of (W -SUP(SO)_category ) c= the carrier of (W -SUP_category ) by ALTCAT_2:def 11;

      

       A3: the carrier of (W -CL-opp_category ) c= the carrier of (W -SUP(SO)_category ) by ALTCAT_2:def 11;

      let L be LATTICE;

      assume

       A4: the carrier of L in W;

      hereby

        assume

         A5: L is Object of (W -CL-opp_category );

        then L in the carrier of (W -CL-opp_category );

        then

        reconsider a = L as Object of (W -SUP(SO)_category ) by A3;

        

         A6: a in the carrier of (W -SUP(SO)_category );

        ( latt a) is continuous by A5, Def13;

        hence L is strict complete continuous by A1, A2, A6, Def5;

      end;

      assume

       A7: L is strict complete continuous;

      then L is Object of (W -SUP_category ) by A4, Def5;

      then

      reconsider a = L as Object of (W -SUP(SO)_category ) by Def11;

      ( latt a) = L;

      hence thesis by A7, Def13;

    end;

    theorem :: WAYBEL34:51

    

     Th51: for W be with_non-empty_element set holds for a,b be Object of (W -CL-opp_category ) holds for f be set holds f in <^a, b^> iff ex g be sups-preserving Function of ( latt a), ( latt b) st g = f & ( UpperAdj g) is directed-sups-preserving

    proof

      let W be with_non-empty_element set;

      let a,b be Object of (W -CL-opp_category ), f be set;

      the carrier of (W -CL-opp_category ) c= the carrier of (W -SUP(SO)_category ) by ALTCAT_2:def 11;

      then

      reconsider a1 = a, b1 = b as Object of (W -SUP(SO)_category );

       <^a, b^> = <^a1, b1^> by ALTCAT_2: 28;

      hence thesis by Th46;

    end;

    theorem :: WAYBEL34:52

    

     Th52: for W be with_non-empty_element set holds ((W -INF(SC)_category ),(W -SUP(SO)_category )) are_anti-isomorphic_under (W LowerAdj )

    proof

      let W be with_non-empty_element set;

      set A1 = (W -INF_category );

      set B1 = (W -INF(SC)_category ), B2 = (W -SUP(SO)_category );

      set F = (W LowerAdj );

      

       A1: ex a be non empty set st a in W by SETFAM_1:def 10;

      

       A2: for a be Object of A1 holds a is Object of B1 iff (F . a) is Object of B2 by Def10, Def11;

       A3:

      now

        let a,b be Object of A1 such that

         A4: <^a, b^> <> {} ;

        let a1,b1 be Object of B1 such that

         A5: a1 = a and

         A6: b1 = b;

        let a2,b2 be Object of B2 such that

         A7: a2 = (F . a) and

         A8: b2 = (F . b);

        let f be Morphism of a, b;

        

         A9: <^(F . b), (F . a)^> <> {} by A4, FUNCTOR0:def 19;

        

         A10: ( @ f) = f by A4, YELLOW21:def 7;

        

         A11: ( @ (F . f)) = (F . f) by A9, YELLOW21:def 7;

        

         A12: (F . a) = ( latt a) by Def6;

        

         A13: (F . b) = ( latt b) by Def6;

        

         A14: (F . f) = ( LowerAdj ( @ f)) by A4, Def6;

        reconsider g = f as infs-preserving Function of ( latt a1), ( latt b1) by A1, A4, A5, A6, A10, Def4;

        ( UpperAdj ( LowerAdj g)) = g by Th10;

        then f in <^a1, b1^> iff ( UpperAdj ( LowerAdj g)) is directed-sups-preserving by A4, A5, A6, A10, Def10;

        hence f in <^a1, b1^> iff (F . f) in <^b2, a2^> by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Def11;

      end;

      thus thesis by A2, A3, YELLOW20: 57;

    end;

    theorem :: WAYBEL34:53

    for W be with_non-empty_element set holds ((W -SUP(SO)_category ),(W -INF(SC)_category )) are_anti-isomorphic_under (W UpperAdj )

    proof

      let W be with_non-empty_element set;

      ((W -SUP(SO)_category ),(W -INF(SC)_category )) are_anti-isomorphic_under ((W LowerAdj ) " ) by Th52, YELLOW20: 51;

      hence thesis by Th18;

    end;

    theorem :: WAYBEL34:54

    

     Th54: for W be with_non-empty_element set holds ((W -CL_category ),(W -CL-opp_category )) are_anti-isomorphic_under (W LowerAdj )

    proof

      let W be with_non-empty_element set;

      set A1 = (W -INF_category ), A2 = (W -SUP_category );

      reconsider B1 = (W -CL_category ) as non empty subcategory of A1 by ALTCAT_4: 36;

      reconsider B2 = (W -CL-opp_category ) as non empty subcategory of A2 by ALTCAT_4: 36;

      set F = (W LowerAdj );

      

       A1: ex a be non empty set st a in W by SETFAM_1:def 10;

      

       A2: for a be Object of A1 holds a is Object of B1 iff (F . a) is Object of B2

      proof

        let a be Object of A1;

        

         A3: (F . a) = ( latt a) by Def6;

        

         A4: the carrier of ( latt a) in W by A1, Def4;

        then a is Object of B1 iff ( latt a) is strict complete continuous by Th48;

        hence thesis by A3, A4, Th50;

      end;

       A5:

      now

        let a,b be Object of A1 such that

         A6: <^a, b^> <> {} ;

        let a1,b1 be Object of B1 such that

         A7: a1 = a and

         A8: b1 = b;

        let a2,b2 be Object of B2 such that

         A9: a2 = (F . a) and

         A10: b2 = (F . b);

        let f be Morphism of a, b;

        

         A11: ( @ f) = f by A6, YELLOW21:def 7;

        

         A12: (F . a) = ( latt a) by Def6;

        

         A13: (F . b) = ( latt b) by Def6;

        

         A14: (F . f) = ( LowerAdj ( @ f)) by A6, Def6;

        reconsider g = f as infs-preserving Function of ( latt a1), ( latt b1) by A1, A6, A7, A8, A11, Def4;

        

         A15: ( UpperAdj ( LowerAdj g)) = g by Th10;

        then f in <^a1, b1^> iff ( UpperAdj ( LowerAdj g)) is directed-sups-preserving by Th49;

        hence f in <^a1, b1^> implies (F . f) in <^b2, a2^> by A7, A8, A9, A10, A11, A12, A13, A14, Th51;

        assume (F . f) in <^b2, a2^>;

        then ex g be sups-preserving Function of ( latt b2), ( latt a2) st (F . f) = g & ( UpperAdj g) is directed-sups-preserving by Th51;

        hence f in <^a1, b1^> by A7, A8, A9, A10, A11, A12, A13, A14, A15, Th49;

      end;

      (B1,B2) are_anti-isomorphic_under F by A2, A5, YELLOW20: 57;

      hence thesis;

    end;

    theorem :: WAYBEL34:55

    for W be with_non-empty_element set holds ((W -CL-opp_category ),(W -CL_category )) are_anti-isomorphic_under (W UpperAdj )

    proof

      let W be with_non-empty_element set;

      set A1 = (W -INF_category ), A2 = (W -SUP_category );

      reconsider B1 = (W -CL_category ) as non empty subcategory of A1 by ALTCAT_4: 36;

      reconsider B2 = (W -CL-opp_category ) as non empty subcategory of A2 by ALTCAT_4: 36;

      (B2,B1) are_anti-isomorphic_under ((W LowerAdj ) " ) by Th54, YELLOW20: 51;

      hence thesis by Th18;

    end;

    begin

    definition

      let S,T be non empty reflexive RelStr;

      let f be Function of S, T;

      :: WAYBEL34:def14

      attr f is compact-preserving means for s be Element of S st s is compact holds (f . s) is compact;

    end

    theorem :: WAYBEL34:56

    

     Th56: for S,T be complete LATTICE, d be sups-preserving Function of T, S st d is waybelow-preserving holds d is compact-preserving

    proof

      let S,T be complete LATTICE, d be sups-preserving Function of T, S such that

       A1: for t,t9 be Element of T st t << t9 holds (d . t) << (d . t9);

      let t be Element of T;

      assume t << t;

      hence (d . t) << (d . t) by A1;

    end;

    theorem :: WAYBEL34:57

    

     Th57: for S,T be complete LATTICE, d be sups-preserving Function of T, S st T is algebraic & d is compact-preserving holds d is waybelow-preserving

    proof

      let S,T be complete LATTICE, d be sups-preserving Function of T, S such that

       A1: T is algebraic and

       A2: for t be Element of T st t is compact holds (d . t) is compact;

      let t,t9 be Element of T;

      assume t << t9;

      then

      consider k be Element of T such that

       A3: k in the carrier of ( CompactSublatt T) and

       A4: t <= k and

       A5: k <= t9 by A1, WAYBEL_8: 7;

      k is compact by A3, WAYBEL_8:def 1;

      then (d . k) is compact by A2;

      then

       A6: (d . k) << (d . k);

      

       A7: (d . t) <= (d . k) by A4, WAYBEL_1:def 2;

      (d . k) <= (d . t9) by A5, WAYBEL_1:def 2;

      hence thesis by A6, A7, WAYBEL_3: 2;

    end;

    theorem :: WAYBEL34:58

    

     Th58: for R,S,T be non empty RelStr, X be Subset of R holds for f be Function of R, S holds for g be Function of S, T st f preserves_sup_of X & g preserves_sup_of (f .: X) holds (g * f) preserves_sup_of X

    proof

      let R,S,T be non empty RelStr, X be Subset of R;

      let f be Function of R, S;

      let g be Function of S, T such that

       A1: ex_sup_of (X,R) implies ex_sup_of ((f .: X),S) & ( sup (f .: X)) = (f . ( sup X)) and

       A2: ex_sup_of ((f .: X),S) implies ex_sup_of ((g .: (f .: X)),T) & ( sup (g .: (f .: X))) = (g . ( sup (f .: X)));

      

       A3: (g .: (f .: X)) = ((g * f) .: X) by RELAT_1: 126;

      assume ex_sup_of (X,R);

      hence thesis by A1, A2, A3, FUNCT_2: 15;

    end;

    definition

      let S,T be non empty RelStr;

      let f be Function of S, T;

      :: WAYBEL34:def15

      attr f is finite-sups-preserving means for X be finite Subset of S holds f preserves_sup_of X;

      :: WAYBEL34:def16

      attr f is bottom-preserving means f preserves_sup_of ( {} S);

    end

    theorem :: WAYBEL34:59

    for R,S,T be non empty RelStr holds for f be Function of R, S holds for g be Function of S, T st f is finite-sups-preserving & g is finite-sups-preserving holds (g * f) is finite-sups-preserving

    proof

      let R,S,T be non empty RelStr;

      let f be Function of R, S;

      let g be Function of S, T such that

       A1: for X be finite Subset of R holds f preserves_sup_of X and

       A2: for X be finite Subset of S holds g preserves_sup_of X;

      let X be finite Subset of R;

      g preserves_sup_of (f .: X) by A2;

      hence thesis by A1, Th58;

    end;

    definition

      let S,T be non empty antisymmetric lower-bounded RelStr;

      let f be Function of S, T;

      :: original: bottom-preserving

      redefine

      :: WAYBEL34:def17

      attr f is bottom-preserving means

      : Def17: (f . ( Bottom S)) = ( Bottom T);

      compatibility

      proof

        thus f is bottom-preserving implies (f . ( Bottom S)) = ( Bottom T)

        proof

          assume f preserves_sup_of ( {} S);

          then ex_sup_of (( {} S),S) implies ( sup (f .: ( {} S))) = (f . ( sup ( {} S)));

          hence thesis by YELLOW_0: 42;

        end;

        assume that

         A1: (f . ( Bottom S)) = ( Bottom T) and ex_sup_of (( {} S),S);

        thus ex_sup_of ((f .: ( {} S)),T) by YELLOW_0: 42;

        thus thesis by A1;

      end;

    end

    definition

      let L be non empty RelStr;

      let S be SubRelStr of L;

      :: WAYBEL34:def18

      attr S is finite-sups-inheriting means for X be finite Subset of S st ex_sup_of (X,L) holds ( "\/" (X,L)) in the carrier of S;

      :: WAYBEL34:def19

      attr S is bottom-inheriting means

      : Def19: ( Bottom L) in the carrier of S;

    end

    registration

      let S,T be non empty RelStr;

      cluster sups-preserving -> bottom-preserving for Function of S, T;

      coherence ;

    end

    registration

      let L be lower-bounded antisymmetric non empty RelStr;

      cluster finite-sups-inheriting -> bottom-inheriting join-inheriting for SubRelStr of L;

      coherence

      proof

        let S be SubRelStr of L;

        assume

         A1: S is finite-sups-inheriting;

        then ex_sup_of ( {} ,L) implies ( "\/" (( {} S),L)) in the carrier of S;

        hence ( Bottom L) in the carrier of S by YELLOW_0: 42;

        let x,y be Element of L;

        assume that

         A2: x in the carrier of S and

         A3: y in the carrier of S;

        reconsider X = {x, y} as finite Subset of S by A2, A3, ZFMISC_1: 32;

         ex_sup_of (X,L) implies ( "\/" (X,L)) in the carrier of S by A1;

        hence thesis;

      end;

    end

    registration

      let L be non empty RelStr;

      cluster sups-inheriting -> finite-sups-inheriting for SubRelStr of L;

      coherence ;

    end

    registration

      let S,T be lower-bounded non empty Poset;

      cluster sups-preserving for Function of S, T;

      existence

      proof

        set f = the sups-preserving Function of S, T;

        take f;

        thus thesis;

      end;

    end

    registration

      let L be lower-bounded antisymmetric non empty RelStr;

      cluster bottom-inheriting -> non empty lower-bounded for full SubRelStr of L;

      coherence

      proof

        let S be full SubRelStr of L;

        assume

         A1: ( Bottom L) in the carrier of S;

        hence

         A2: S is non empty;

        reconsider x = ( Bottom L) as Element of S by A1;

        take x;

        let y be Element of S;

        assume

         A3: y in the carrier of S;

        reconsider a = y as Element of L by A2, YELLOW_0: 58;

        ( Bottom L) <= a by YELLOW_0: 44;

        hence thesis by A3, YELLOW_0: 60;

      end;

    end

    registration

      let L be lower-bounded antisymmetric non empty RelStr;

      cluster non empty sups-inheriting finite-sups-inheriting bottom-inheriting full for SubRelStr of L;

      existence

      proof

        set S = the non empty sups-inheriting full SubRelStr of L;

        take S;

        thus thesis;

      end;

    end

    theorem :: WAYBEL34:60

    

     Th60: for L be lower-bounded antisymmetric non empty RelStr holds for S be non empty bottom-inheriting full SubRelStr of L holds ( Bottom S) = ( Bottom L)

    proof

      let L be lower-bounded antisymmetric non empty RelStr;

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

      reconsider s = ( Bottom L) as Element of S by Def19;

      reconsider l = ( Bottom S) as Element of L by YELLOW_0: 58;

      

       A1: ( Bottom L) <= l by YELLOW_0: 44;

      

       A2: ( Bottom S) <= s by YELLOW_0: 44;

      ( Bottom S) >= s by A1, YELLOW_0: 60;

      hence thesis by A2, ORDERS_2: 2;

    end;

    registration

      let L be with_suprema lower-bounded non empty Poset;

      cluster bottom-inheriting join-inheriting -> finite-sups-inheriting for full SubRelStr of L;

      coherence

      proof

        let S be full SubRelStr of L;

        assume S is bottom-inheriting join-inheriting;

        then

        reconsider S9 = S as join-inheriting bottom-inheriting full SubRelStr of L;

        let X be finite Subset of S;

        reconsider X9 = X as Subset of S9;

        

         A1: X is finite;

        defpred P[ set] means for Y be finite Subset of S9 st Y = $1 holds ex_sup_of (Y,L) & ( "\/" (Y,L)) = ( sup Y);

        

         A2: ( Bottom L) = ( "\/" ( {} ,L));

        ( Bottom S9) = ( "\/" ( {} ,S9));

        then

         A3: P[ {} ] by A2, Th60, YELLOW_0: 42;

        

         A4: for x,B be set st x in X & B c= X & P[B] holds P[(B \/ {x})]

        proof

          let x,B be set such that x in X and B c= X and

           A5: for Y be finite Subset of S9 st Y = B holds ex_sup_of (Y,L) & ( "\/" (Y,L)) = ( sup Y);

          let Y be finite Subset of S9 such that

           A6: Y = (B \/ {x});

          

           A7: B c= Y by A6, XBOOLE_1: 7;

          

           A8: {x} c= Y by A6, XBOOLE_1: 7;

          reconsider Z = B as finite Subset of S9 by A7, XBOOLE_1: 1;

          

           A9: ex_sup_of (Z,L) by A5;

          

           A10: ( "\/" (Z,L)) = ( sup Z) by A5;

          x in Y by A8, ZFMISC_1: 31;

          then

          reconsider x as Element of S9;

          reconsider a = x as Element of L by YELLOW_0: 58;

          

           A11: ex_sup_of ( {a},L) by YELLOW_0: 38;

          hence ex_sup_of (Y,L) by A6, A9, YELLOW_2: 3;

          

           A12: Z = {} or Z <> {} & S9 is with_suprema;

          

           A13: ex_sup_of ( {x},S9) by YELLOW_0: 54;

          

           A14: ex_sup_of (Z,S9) by A12, YELLOW_0: 42, YELLOW_0: 54;

          

          thus ( "\/" (Y,L)) = (( "\/" (Z,L)) "\/" ( sup {a})) by A6, A9, A11, YELLOW_2: 3

          .= (( "\/" (Z,L)) "\/" a) by YELLOW_0: 39

          .= (( sup Z) "\/" x) by A10, YELLOW_0: 70

          .= (( sup Z) "\/" ( sup {x})) by YELLOW_0: 39

          .= ( sup Y) by A6, A13, A14, YELLOW_2: 3;

        end;

         P[X] from FINSET_1:sch 2( A1, A3, A4);

        then ( "\/" (X,L)) = ( sup X9);

        hence thesis;

      end;

    end

    theorem :: WAYBEL34:61

    for S,T be non empty RelStr, f be Function of S, T st f is finite-sups-preserving holds f is join-preserving bottom-preserving;

    theorem :: WAYBEL34:62

    

     Th62: for S,T be lower-bounded with_suprema Poset, f be Function of S, T st f is join-preserving bottom-preserving holds f is finite-sups-preserving

    proof

      let S,T be lower-bounded with_suprema Poset, f be Function of S, T;

      assume

       A1: f is join-preserving bottom-preserving;

      let X be finite Subset of S;

      

       A2: X is finite;

      defpred P[ set] means for Y be finite Subset of S st Y = $1 holds f preserves_sup_of Y;

      f preserves_sup_of ( {} S) by A1;

      then

       A3: P[ {} ];

      

       A4: for x,B be set st x in X & B c= X & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that x in X and B c= X and

         A5: for Y be finite Subset of S st Y = B holds f preserves_sup_of Y;

        let Y be finite Subset of S such that

         A6: Y = (B \/ {x});

        

         A7: B c= Y by A6, XBOOLE_1: 7;

        

         A8: {x} c= Y by A6, XBOOLE_1: 7;

        reconsider Z = B as finite Subset of S by A7, XBOOLE_1: 1;

        

         A9: x in Y by A8, ZFMISC_1: 31;

        then

        reconsider x as Element of S;

        

         A10: f preserves_sup_of Z by A5;

        (f .: Z) = {} or (f .: Z) <> {} & (f .: Z) is finite;

        then

         A11: ex_sup_of ((f .: Z),T) by YELLOW_0: 42, YELLOW_0: 54;

        

         A12: ex_sup_of ( {(f . x)},T) by YELLOW_0: 54;

        Z = {} or Z <> {} ;

        then

         A13: ex_sup_of (Z,S) by YELLOW_0: 42, YELLOW_0: 54;

        

         A14: f preserves_sup_of {( sup Z), x} by A1;

        

         A15: ( sup {x}) = x by YELLOW_0: 39;

        

         A16: ex_sup_of ( {x},S) by YELLOW_0: 38;

        

         A17: ex_sup_of (Y,S) by A9, YELLOW_0: 54;

        assume ex_sup_of (Y,S);

        thus ex_sup_of ((f .: Y),T) by A9, YELLOW_0: 54;

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

        then ( Im (f,x)) = {(f . x)} by FUNCT_1: 59;

        then

         A18: (f .: Y) = ((f .: Z) \/ {(f . x)}) by A6, RELAT_1: 120;

        ( sup {(f . x)}) = (f . x) by YELLOW_0: 39;

        

        hence ( sup (f .: Y)) = (( sup (f .: Z)) "\/" (f . x)) by A11, A12, A18, YELLOW_2: 3

        .= ((f . ( sup Z)) "\/" (f . x)) by A10, A13

        .= (f . (( sup Z) "\/" x)) by A14, YELLOW_3: 9

        .= (f . ( sup Y)) by A6, A13, A15, A16, A17, YELLOW_0: 36;

      end;

       P[X] from FINSET_1:sch 2( A2, A3, A4);

      hence thesis;

    end;

    registration

      let S,T be non empty RelStr;

      cluster sups-preserving -> finite-sups-preserving for Function of S, T;

      coherence ;

      cluster finite-sups-preserving -> join-preserving bottom-preserving for Function of S, T;

      coherence ;

    end

    registration

      let S be non empty RelStr;

      let T be lower-bounded non empty reflexive antisymmetric RelStr;

      cluster sups-preserving finite-sups-preserving for Function of S, T;

      existence

      proof

        set f = the sups-preserving Function of S, T;

        take f;

        thus thesis;

      end;

    end

    registration

      let L be lower-bounded non empty Poset;

      cluster ( CompactSublatt L) -> lower-bounded;

      coherence

      proof

        ( Bottom L) is compact by WAYBEL_3: 15;

        then

        reconsider c = ( Bottom L) as Element of ( CompactSublatt L) by WAYBEL_8:def 1;

        take c;

        let b be Element of ( CompactSublatt L) such that b in the carrier of ( CompactSublatt L);

        reconsider x = b as Element of L by YELLOW_0: 58;

        ( Bottom L) <= x by YELLOW_0: 44;

        hence c <= b by YELLOW_0: 60;

      end;

    end

    theorem :: WAYBEL34:63

    

     Th63: for S be RelStr, T be non empty RelStr, f be Function of S, T holds for S9 be SubRelStr of S holds for T9 be SubRelStr of T st (f .: the carrier of S9) c= the carrier of T9 holds (f | the carrier of S9) is Function of S9, T9

    proof

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

      let S9 be SubRelStr of S, T9 be SubRelStr of T such that

       A1: (f .: the carrier of S9) c= the carrier of T9;

      set g = (f | the carrier of S9);

      

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

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

      then

       A3: ( dom g) = the carrier of S9 by A2, RELAT_1: 62;

      ( rng g) = (f .: the carrier of S9) by RELAT_1: 115;

      hence thesis by A1, A3, FUNCT_2: 2;

    end;

    theorem :: WAYBEL34:64

    

     Th64: for S,T be LATTICE, f be join-preserving Function of S, T holds for S9 be non empty join-inheriting full SubRelStr of S holds for T9 be non empty join-inheriting full SubRelStr of T holds for g be Function of S9, T9 st g = (f | the carrier of S9) holds g is join-preserving

    proof

      let S,T be LATTICE, f be join-preserving Function of S, T;

      let S9 be non empty join-inheriting full SubRelStr of S;

      let T9 be non empty join-inheriting full SubRelStr of T;

      let g be Function of S9, T9 such that

       A1: g = (f | the carrier of S9);

      now

        let x,y be Element of S9;

        reconsider a = x, b = y as Element of S by YELLOW_0: 58;

        (x "\/" y) = (a "\/" b) by YELLOW_0: 70;

        then

         A2: (g . (x "\/" y)) = (f . (a "\/" b)) by A1, FUNCT_1: 49;

        

         A3: (g . x) = (f . a) by A1, FUNCT_1: 49;

        

         A4: (g . y) = (f . b) by A1, FUNCT_1: 49;

        

        thus (g . (x "\/" y)) = ((f . a) "\/" (f . b)) by A2, WAYBEL_6: 2

        .= ((g . x) "\/" (g . y)) by A3, A4, YELLOW_0: 70;

      end;

      hence thesis by WAYBEL_6: 2;

    end;

    theorem :: WAYBEL34:65

    

     Th65: for S,T be lower-bounded LATTICE holds for f be finite-sups-preserving Function of S, T holds for S9 be non empty finite-sups-inheriting full SubRelStr of S holds for T9 be non empty finite-sups-inheriting full SubRelStr of T holds for g be Function of S9, T9 st g = (f | the carrier of S9) holds g is finite-sups-preserving

    proof

      let S,T be lower-bounded LATTICE;

      let f be finite-sups-preserving Function of S, T;

      let S9 be non empty finite-sups-inheriting full SubRelStr of S;

      let T9 be non empty finite-sups-inheriting full SubRelStr of T;

      let g be Function of S9, T9 such that

       A1: g = (f | the carrier of S9);

      ( Bottom S9) = ( Bottom S) by Th60;

      

      then (g . ( Bottom S9)) = (f . ( Bottom S)) by A1, FUNCT_1: 49

      .= ( Bottom T) by Def17

      .= ( Bottom T9) by Th60;

      then g is bottom-preserving;

      hence thesis by A1, Th62, Th64;

    end;

    registration

      let L be complete LATTICE;

      cluster ( CompactSublatt L) -> finite-sups-inheriting;

      coherence

      proof

        ( Bottom L) in the carrier of ( CompactSublatt L) by WAYBEL_8: 3;

        then ( CompactSublatt L) is bottom-inheriting join-inheriting non empty full SubRelStr of L by Def19;

        hence thesis;

      end;

    end

    theorem :: WAYBEL34:66

    

     Th66: for S,T be complete LATTICE holds for d be sups-preserving Function of T, S holds d is compact-preserving iff (d | the carrier of ( CompactSublatt T)) is finite-sups-preserving Function of ( CompactSublatt T), ( CompactSublatt S)

    proof

      let S,T be complete LATTICE, d be sups-preserving Function of T, S;

      thus d is compact-preserving implies (d | the carrier of ( CompactSublatt T)) is finite-sups-preserving Function of ( CompactSublatt T), ( CompactSublatt S)

      proof

        assume

         A1: for x be Element of T st x is compact holds (d . x) is compact;

        (d .: the carrier of ( CompactSublatt T)) c= the carrier of ( CompactSublatt S)

        proof

          let y be object;

          assume y in (d .: the carrier of ( CompactSublatt T));

          then

          consider x be object such that

           A2: x in the carrier of T and

           A3: x in the carrier of ( CompactSublatt T) and

           A4: y = (d . x) by FUNCT_2: 64;

          reconsider x as Element of T by A2;

          x is compact by A3, WAYBEL_8:def 1;

          then (d . x) is compact by A1;

          hence thesis by A4, WAYBEL_8:def 1;

        end;

        hence thesis by Th63, Th65;

      end;

      assume

       A5: (d | the carrier of ( CompactSublatt T)) is finite-sups-preserving Function of ( CompactSublatt T), ( CompactSublatt S);

      let x be Element of T;

      assume x is compact;

      then

       A6: x in the carrier of ( CompactSublatt T) by WAYBEL_8:def 1;

      then (d . x) = ((d | the carrier of ( CompactSublatt T)) . x) by FUNCT_1: 49;

      then (d . x) in the carrier of ( CompactSublatt S) by A5, A6, FUNCT_2: 5;

      hence thesis by WAYBEL_8:def 1;

    end;

    theorem :: WAYBEL34:67

    for S,T be complete LATTICE st T is algebraic holds for g be infs-preserving Function of S, T holds g is directed-sups-preserving iff (( LowerAdj g) | the carrier of ( CompactSublatt T)) is finite-sups-preserving Function of ( CompactSublatt T), ( CompactSublatt S)

    proof

      let S,T be complete LATTICE such that

       A1: T is algebraic;

      let g be infs-preserving Function of S, T;

      hereby

        assume g is directed-sups-preserving;

        then ( LowerAdj g) is waybelow-preserving by Th22;

        then ( LowerAdj g) is compact-preserving by Th56;

        hence (( LowerAdj g) | the carrier of ( CompactSublatt T)) is finite-sups-preserving Function of ( CompactSublatt T), ( CompactSublatt S) by Th66;

      end;

      assume (( LowerAdj g) | the carrier of ( CompactSublatt T)) is finite-sups-preserving Function of ( CompactSublatt T), ( CompactSublatt S);

      then ( LowerAdj g) is compact-preserving by Th66;

      then ( LowerAdj g) is waybelow-preserving by A1, Th57;

      hence thesis by A1, Th23;

    end;