yellow21.miz



    begin

    reserve x,y for set;

    definition

      let a be object;

      :: YELLOW21:def1

      func a as_1-sorted -> 1-sorted equals

      : Def1: a if a is 1-sorted

      otherwise the 1-sorted;

      coherence ;

      consistency ;

    end

    definition

      let W be set;

      defpred P[ object] means $1 is strict Poset & the carrier of ($1 as_1-sorted ) in W;

      :: YELLOW21:def2

      func POSETS W -> set means

      : Def2: for x be object holds x in it iff x is strict Poset & the carrier of (x as_1-sorted ) in W;

      uniqueness

      proof

        let A,B be set such that

         A1: for x be object holds x in A iff P[x] and

         A2: for x be object holds x in B iff P[x];

        thus thesis from XBOOLE_0:sch 2( A1, A2);

      end;

      existence

      proof

        defpred Q[ object, object] means ex P be strict Poset st $2 = P & the InternalRel of P = $1;

        defpred P[ set, set] means $2 is Order of $1;

        deffunc F( set) = ( bool [:$1, $1:]);

        consider F be Function such that

         A3: ( dom F) = W and

         A4: for x st x in W holds for y holds y in (F . x) iff y in F(x) & P[x, y] from CARD_3:sch 3;

         A5:

        now

          let x,y,z be object;

          assume Q[x, y];

          then

          consider P1 be strict Poset such that

           A6: y = P1 & the InternalRel of P1 = x;

          

           A7: ( dom the InternalRel of P1) = the carrier of P1 by ORDERS_1: 14;

          assume Q[x, z];

          hence y = z by A6, A7, ORDERS_1: 14;

        end;

        consider A be set such that

         A8: for x be object holds x in A iff ex y be object st y in ( Union F) & Q[y, x] from TARSKI:sch 1( A5);

        take A;

        let x be object;

        hereby

          assume x in A;

          then

          consider y be object such that

           A9: y in ( Union F) and

           A10: ex P be strict Poset st x = P & the InternalRel of P = y by A8;

          consider P be strict Poset such that

           A11: x = P and

           A12: the InternalRel of P = y by A10;

          thus x is strict Poset by A11;

          consider z be object such that

           A13: z in W and

           A14: y in (F . z) by A3, A9, CARD_5: 2;

          reconsider z as set by TARSKI: 1;

          reconsider y as Order of z by A4, A13, A14;

          ( dom y) = z & ( dom y) = the carrier of P by A12, ORDERS_1: 14;

          hence the carrier of (x as_1-sorted ) in W by A11, A13, Def1;

        end;

        assume that

         A15: x is strict Poset and

         A16: the carrier of (x as_1-sorted ) in W;

        reconsider P = x as strict Poset by A15;

        

         A17: (x as_1-sorted ) = P by Def1;

        then the InternalRel of P in (F . the carrier of P) by A4, A16;

        then the InternalRel of P in ( Union F) by A3, A16, A17, CARD_5: 2;

        hence thesis by A8;

      end;

    end

    registration

      let W be non empty set;

      cluster ( POSETS W) -> non empty;

      coherence

      proof

        set x = the Element of W, y = the Order of x;

        ( RelStr (# x, y #) as_1-sorted ) = RelStr (# x, y #) by Def1;

        hence thesis by Def2;

      end;

    end

    registration

      let W be with_non-empty_elements set;

      cluster ( POSETS W) -> POSet_set-like;

      coherence

      proof

        let a be set;

        assume

         A1: a in ( POSETS W);

        then

         A2: the carrier of (a as_1-sorted ) in W by Def2;

        reconsider a as Poset by A1, Def2;

        a = (a as_1-sorted ) by Def1;

        hence thesis by A2;

      end;

    end

    definition

      let C be category;

      :: YELLOW21:def3

      attr C is carrier-underlaid means

      : Def3: for a be Object of C holds ex S be 1-sorted st a = S & ( the_carrier_of a) = the carrier of S;

    end

    definition

      let C be category;

      :: YELLOW21:def4

      attr C is lattice-wise means

      : Def4: C is semi-functional set-id-inheriting & (for a be Object of C holds a is LATTICE) & for a,b be Object of C holds for A,B be LATTICE st A = a & B = b holds <^a, b^> c= ( MonFuncs (A,B));

    end

    definition

      let C be category;

      :: YELLOW21:def5

      attr C is with_complete_lattices means

      : Def5: C is lattice-wise & for a be Object of C holds a is complete LATTICE;

    end

    registration

      cluster with_complete_lattices -> lattice-wise for category;

      coherence ;

      cluster lattice-wise -> concrete carrier-underlaid for category;

      coherence

      proof

        deffunc F( set) = the carrier of ($1 as_1-sorted );

        let C be category such that

         A1: C is semi-functional set-id-inheriting and

         A2: for a be Object of C holds a is LATTICE and

         A3: for a,b be Object of C holds for A,B be LATTICE st A = a & B = b holds <^a, b^> c= ( MonFuncs (A,B));

        consider F be ManySortedSet of C such that

         A4: for i be Element of C holds (F . i) = F(i) from PBOOLE:sch 5;

        C is para-functional

        proof

          take F;

          let a,b be Object of C;

          reconsider A = a, B = b as LATTICE by A2;

          

           A5: <^a, b^> c= ( MonFuncs (A,B)) by A3;

          (b as_1-sorted ) = B by Def1;

          then

           A6: (F . b) = the carrier of B by A4;

          (a as_1-sorted ) = A by Def1;

          then (F . a) = the carrier of A by A4;

          then ( MonFuncs (A,B)) c= ( Funcs ((F . a),(F . b))) by A6, ORDERS_3: 11;

          hence thesis by A5;

        end;

        hence C is concrete by A1;

        let a be Object of C;

        reconsider S = a as LATTICE by A2;

        ( idm a) in <^a, a^> & <^a, a^> c= ( MonFuncs (S,S)) by A3;

        then

        consider f be Function of S, S such that

         A7: ( idm a) = f and

         A8: f in ( Funcs (the carrier of S,the carrier of S)) and f is monotone by ORDERS_3:def 6;

        take S;

        thus a = S;

        

        thus ( the_carrier_of a) = ( dom ( id ( the_carrier_of a))) by RELAT_1: 45

        .= ( dom f) by A1, A7

        .= the carrier of S by A8, FUNCT_2: 92;

      end;

    end

    scheme :: YELLOW21:sch1

    localCLCatEx { A() -> non empty set , P[ object, object, object] } :

ex C be strict category st C is lattice-wise & the carrier of C = A() & for a,b be LATTICE, f be monotone Function of a, b holds f in (the Arrows of C . (a,b)) iff a in A() & b in A() & P[a, b, f]

      provided

       A1: for a be Element of A() holds a is LATTICE

       and

       A2: for a,b,c be LATTICE st a in A() & b in A() & c in A() 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)]

       and

       A3: for a be LATTICE st a in A() holds P[a, a, ( id a)];

      defpred P[ object, object] means ex a,b be LATTICE, c be set st c = $2 & $1 = [a, b] & for f be object holds f in c iff f in ( MonFuncs (a,b)) & P[a, b, f];

      set A = A();

       A4:

      now

        let x be object;

        assume x in [:A, A:];

        then

        consider a,b be object such that

         A5: a in A & b in A and

         A6: x = [a, b] by ZFMISC_1:def 2;

        reconsider a, b as LATTICE by A1, A5;

        defpred Q[ object] means P[a, b, $1];

        consider y be set such that

         A7: for f be object holds f in y iff f in ( MonFuncs (a,b)) & Q[f] from XBOOLE_0:sch 1;

        reconsider y as object;

        take y;

        thus P[x, y] by A6, A7;

      end;

      consider F be Function such that ( dom F) = [:A, A:] and

       A8: for x be object st x in [:A, A:] holds P[x, (F . x)] from CLASSES1:sch 1( A4);

      defpred PP[ object, object] means for a be LATTICE st a = $1 holds $2 = the carrier of a;

       A9:

      now

        let x be object;

        assume x in A;

        then

        reconsider a = x as LATTICE by A1;

        reconsider b = the carrier of a as object;

        take b;

        thus PP[x, b];

      end;

      consider D be Function such that ( dom D) = A and

       A10: for x be object st x in A holds PP[x, (D . x)] from CLASSES1:sch 1( A9);

      deffunc B( set, set) = (F . [$1, $2]);

       A11:

      now

        let a,b be LATTICE;

        assume a in A & b in A;

        then [a, b] in [:A, A:] by ZFMISC_1: 87;

        then P[ [a, b], (F . [a, b])] by A8;

        then

        consider a9,b9 be LATTICE, c be set such that

         A12: c = (F . [a, b]) and

         A13: [a, b] = [a9, b9] and

         A14: for f be object holds f in c iff f in ( MonFuncs (a9,b9)) & P[a9, b9, f];

        let f be set;

        

         A15: a = a9 & b = b9 by A13, XTUPLE_0: 1;

        hereby

          assume

           A16: f in (F . [a, b]);

          hence P[a, b, f] by A14, A15, A12;

          thus f in ( MonFuncs (a,b)) by A14, A15, A16, A12;

          then ex g be Function of a, b st f = g & g in ( Funcs (the carrier of a,the carrier of b)) & g is monotone by ORDERS_3:def 6;

          hence f in ( Funcs (the carrier of a,the carrier of b)) & f is monotone Function of a, b;

        end;

        assume f is monotone Function of a, b;

        then

        reconsider g = f as monotone Function of a, b;

        the carrier of b <> {} implies ( dom g) = the carrier of a & ( rng g) c= the carrier of b by FUNCT_2:def 1;

        then g in ( Funcs (the carrier of a,the carrier of b)) by FUNCT_2:def 2;

        then

         A17: f in ( MonFuncs (a,b)) by ORDERS_3:def 6;

        assume P[a, b, f];

        then f in c by A14, A15, A17;

        hence f in (F . [a, b]) by A12;

      end;

      

       A18: for a,b,c be Element of A, f,g be Function st f in B(a,b) & g in B(b,c) holds (g * f) in B(a,c)

      proof

        let a,b,c be Element of A, f,g be Function such that

         A19: f in (F . [a, b]) and

         A20: g in (F . [b, c]);

        reconsider x = a, y = b, z = c as LATTICE by A1;

        reconsider g9 = g as monotone Function of y, z by A11, A20;

        reconsider f9 = f as monotone Function of x, y by A11, A19;

        P[x, y, f9] & P[y, z, g9] by A11, A19, A20;

        then P[a, c, (g9 * f9)] by A2;

        then (g9 * f9) is monotone Function of x, z implies (g9 * f9) in (F . [x, z]) by A11;

        hence thesis by YELLOW_2: 12;

      end;

      deffunc D( set) = (D . $1);

      

       A21: for a,b be Element of A holds B(a,b) c= ( Funcs ( D(a), D(b)))

      proof

        let a,b be Element of A, f be object;

        reconsider x = a, y = b as LATTICE by A1;

        assume f in (F . [a, b]);

        then f in ( Funcs (the carrier of x,the carrier of y)) by A11;

        then f in ( Funcs ((D . a),the carrier of y)) by A10;

        hence thesis by A10;

      end;

       A22:

      now

        let a be Element of A;

        reconsider x = a as LATTICE by A1;

        ( id (D . a)) = ( id x) & P[x, x, ( id x)] by A3, A10;

        hence ( id D(a)) in B(a,a) by A11;

      end;

      consider C be concrete strict category such that

       A23: the carrier of C = A and for a be Object of C holds ( the_carrier_of a) = D(a) and

       A24: for a,b be Object of C holds <^a, b^> = B(a,b) from YELLOW18:sch 16( A18, A21, A22);

      take C;

      thus C is semi-functional set-id-inheriting;

      thus for a be Object of C holds a is LATTICE by A1, A23;

      thus for a,b be Object of C holds for A,B be LATTICE st A = a & B = b holds <^a, b^> c= ( MonFuncs (A,B))

      proof

        let a,b be Object of C;

        let A,B be LATTICE;

        assume

         A25: A = a & B = b;

        let f be object;

         <^a, b^> = (F . [A, B]) by A24, A25;

        hence thesis by A11, A23, A25;

      end;

      thus the carrier of C = A() by A23;

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

      hereby

        assume

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

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

        then

         A27: [a, b] in [:A, A:] by A23;

        hence a in A & b in A by ZFMISC_1: 87;

        reconsider x = a, y = b as Object of C by A23, A27, ZFMISC_1: 87;

        (the Arrows of C . [a, b]) = <^x, y^>

        .= (F . [x, y]) by A24;

        hence P[a, b, f] by A11, A23, A26;

      end;

      assume

       A28: a in A() & b in A();

      then

      reconsider x = a, y = b as Object of C by A23;

      (the Arrows of C . [a, b]) = <^x, y^>

      .= (F . [x, y]) by A24;

      hence thesis by A11, A28;

    end;

    registration

      cluster strict with_complete_lattices for category;

      existence

      proof

        defpred P[ set, set, set] means $3 = $3;

        set L = the complete LATTICE;

        

         A1: for a,b,c be LATTICE st a in {L} & b in {L} & c in {L} 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)];

        

         A2: for a be LATTICE st a in {L} holds P[a, a, ( id a)];

        

         A3: for a be Element of {L} holds a is LATTICE by TARSKI:def 1;

        consider C be strict category such that

         A4: C is lattice-wise and

         A5: the carrier of C = {L} and for a,b be LATTICE, f be monotone Function of a, b holds f in (the Arrows of C . (a,b)) iff a in {L} & b in {L} & P[a, b, f] from localCLCatEx( A3, A1, A2);

        take C;

        thus C is strict;

        thus C is lattice-wise by A4;

        let a be Object of C;

        thus thesis by A5, TARSKI:def 1;

      end;

    end

    theorem :: YELLOW21:1

    for C be carrier-underlaid category, a be Object of C holds ( the_carrier_of a) = the carrier of (a as_1-sorted )

    proof

      let C be carrier-underlaid category, a be Object of C;

      ex S be 1-sorted st a = S & ( the_carrier_of a) = the carrier of S by Def3;

      hence thesis by Def1;

    end;

    theorem :: YELLOW21:2

    

     Th2: for C be set-id-inheriting carrier-underlaid category holds for a be Object of C holds ( idm a) = ( id (a as_1-sorted ))

    proof

      let C be set-id-inheriting carrier-underlaid category;

      let a be Object of C;

      ex S be 1-sorted st a = S & ( the_carrier_of a) = the carrier of S by Def3;

      then ( the_carrier_of a) = the carrier of (a as_1-sorted ) by Def1;

      hence thesis by YELLOW18:def 10;

    end;

    notation

      let C be lattice-wise category;

      let a be Object of C;

      synonym latt a for a as_1-sorted ;

    end

    definition

      let C be lattice-wise category;

      let a be Object of C;

      :: original: latt

      redefine

      :: YELLOW21:def6

      func latt a -> LATTICE equals a;

      coherence

      proof

        a is LATTICE by Def4;

        hence thesis by Def1;

      end;

      compatibility

      proof

        a is LATTICE by Def4;

        hence thesis by Def1;

      end;

    end

    notation

      let C be with_complete_lattices category;

      let a be Object of C;

      synonym latt a for a as_1-sorted ;

    end

    definition

      let C be with_complete_lattices category;

      let a be Object of C;

      :: original: latt

      redefine

      func latt a -> complete LATTICE ;

      coherence by Def5;

    end

    definition

      let C be lattice-wise category;

      let a,b be Object of C;

      let f be Morphism of a, b;

      :: YELLOW21:def7

      func @ f -> monotone Function of ( latt a), ( latt b) equals

      : Def7: f;

      coherence

      proof

        f in <^a, b^> & <^a, b^> c= ( MonFuncs (( latt a),( latt b))) by A1, Def4;

        then ex g be Function of ( latt a), ( latt b) st f = g & g in ( Funcs (the carrier of ( latt a),the carrier of ( latt b))) & g is monotone by ORDERS_3:def 6;

        hence thesis;

      end;

    end

    theorem :: YELLOW21:3

    

     Th3: for C be lattice-wise category holds for a,b,c be Object of C st <^a, b^> <> {} & <^b, c^> <> {} holds for f be Morphism of a, b, g be Morphism of b, c holds (g * f) = (( @ g) * ( @ f))

    proof

      let C be lattice-wise category;

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

       A1: <^a, b^> <> {} & <^b, c^> <> {} ;

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

      f = ( @ f) & g = ( @ g) by A1, Def7;

      hence thesis by A1, YELLOW18: 36;

    end;

    scheme :: YELLOW21:sch2

    CLCatEx1 { A() -> non empty set , P[ set, set, set] } :

ex C be lattice-wise strict category st the carrier of C = A() & 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]

      provided

       A1: for a be Element of A() holds a is LATTICE

       and

       A2: for a,b,c be LATTICE st a in A() & b in A() & c in A() 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)]

       and

       A3: for a be LATTICE st a in A() holds P[a, a, ( id a)];

      

       A4: for a be LATTICE st a in A() holds P[a, a, ( id a)] by A3;

      

       A5: for a,b,c be LATTICE st a in A() & b in A() & c in A() 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 A2;

      consider C be strict category such that

       A6: C is lattice-wise and

       A7: the carrier of C = A() and

       A8: for a,b be LATTICE, f be monotone Function of a, b holds f in (the Arrows of C . (a,b)) iff a in A() & b in A() & P[a, b, f] from localCLCatEx( A1, A5, A4);

      reconsider C as lattice-wise strict category by A6;

      take C;

      thus the carrier of C = A() by A7;

      let a,b be Object of C;

      thus thesis by A7, A8;

    end;

    scheme :: YELLOW21:sch3

    CLCatEx2 { A() -> non empty set , L[ object], P[ set, set, set] } :

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 A()) & 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]

      provided

       A1: ex x be strict LATTICE st L[x] & the carrier of x in A()

       and

       A2: 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)]

       and

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

      defpred p[ object] means $1 is LATTICE & L[$1];

      consider A be set such that

       A4: for x be object holds x in A iff x in ( POSETS A()) & p[x] from XBOOLE_0:sch 1;

      consider x be strict LATTICE such that

       A5: L[x] and

       A6: the carrier of x in A() by A1;

      (x as_1-sorted ) = x by Def1;

      then x in ( POSETS A()) by A6, Def2;

      then

      reconsider A as non empty set by A4, A5;

       A7:

      now

        let a,b,c be LATTICE;

        assume that

         A8: a in A & b in A and

         A9: c in A;

        

         A10: L[c] by A4, A9;

        L[a] & L[b] by A4, A8;

        hence 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 A2, A10;

      end;

      

       A11: for a be LATTICE st a in A holds P[a, a, ( id a)] by A3, A4;

      

       A12: for a be Element of A holds a is LATTICE by A4;

      consider C be lattice-wise strict category such that

       A13: the carrier of C = A and

       A14: 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 CLCatEx1( A12, A7, A11);

      take C;

      hereby

        let x be LATTICE;

        (x as_1-sorted ) = x by Def1;

        then x in ( POSETS A()) iff x is strict Poset & the carrier of x in A() by Def2;

        hence x is Object of C iff x is strict & L[x] & the carrier of x in A() by A4, A13;

      end;

      thus thesis by A14;

    end;

    scheme :: YELLOW21:sch4

    CLCatUniq1 { A() -> non empty set , P[ set, set, set] } :

for C1,C2 be lattice-wise category st the carrier of C1 = A() & (for a,b be Object of C1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f]) & the carrier of C2 = A() & (for a,b be Object of C2, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f]) holds the AltCatStr of C1 = the AltCatStr of C2;

      let A1,A2 be lattice-wise category;

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

      assume that

       A1: the carrier of A1 = A() and

       A2: for a,b be Object of A1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f] and

       A3: the carrier of A2 = A() and

       A4: for a,b be Object of A2, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f];

       A5:

      now

        let a,b be Object of A2;

        reconsider a9 = a, b9 = b as Object of A1 by A1, A3;

        

         A6: <^a9, b9^> = (the Arrows of A1 . (a9,b9));

        thus <^a, b^> = (the Arrows of A1 . (a,b))

        proof

          hereby

            let x be object;

            assume

             A7: x in <^a, b^>;

            then

            reconsider f = x as Morphism of a, b;

            

             A8: ( @ f) = f by A7, Def7;

            then P[( latt a9), ( latt b9), ( @ f)] by A4, A7;

            hence x in (the Arrows of A1 . (a,b)) by A2, A6, A8;

          end;

          let x be object;

          assume

           A9: x in (the Arrows of A1 . (a,b));

          then

          reconsider f = x as Morphism of a9, b9;

          

           A10: ( @ f) = f by A9, Def7;

          then P[( latt a), ( latt b), ( @ f)] by A2, A9;

          hence thesis by A4, A10;

        end;

      end;

      

       A11: for a,b be Object of A1 holds <^a, b^> = (the Arrows of A1 . (a,b));

      for C1,C2 be para-functional semi-functional category st the carrier of C1 = A() & (for a,b be Object of C1 holds <^a, b^> = B(a,b)) & the carrier of C2 = 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;

      hence thesis by A1, A3, A11, A5;

    end;

    scheme :: YELLOW21:sch5

    CLCatUniq2 { A() -> non empty set , L[ object], P[ set, set, set] } :

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 A()) & (for a,b be Object of C1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f]) & (for x be LATTICE holds x is Object of C2 iff x is strict & L[x] & the carrier of x in A()) & (for a,b be Object of C2, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f]) holds the AltCatStr of C1 = the AltCatStr of C2;

      let A1,A2 be lattice-wise category;

      assume that

       A1: for x be LATTICE holds x is Object of A1 iff x is strict & L[x] & the carrier of x in A() and

       A2: for a,b be Object of A1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f] and

       A3: for x be LATTICE holds x is Object of A2 iff x is strict & L[x] & the carrier of x in A();

      

       A4: the carrier of A2 = the carrier of A1

      proof

        hereby

          let x be object;

          assume

           A5: x in the carrier of A2;

          then

           A6: x is LATTICE by Def4;

          then

           A7: x is strict LATTICE & L[x] by A3, A5;

          

           A8: (x as_1-sorted ) = x by A6, Def1;

          then the carrier of (x as_1-sorted ) in A() by A3, A5, A6;

          then x is Object of A1 by A1, A8, A7;

          hence x in the carrier of A1;

        end;

        let x be object;

        assume

         A9: x in the carrier of A1;

        then

         A10: x is LATTICE by Def4;

        then

         A11: x is strict LATTICE & L[x] by A1, A9;

        

         A12: (x as_1-sorted ) = x by A10, Def1;

        then the carrier of (x as_1-sorted ) in A() by A1, A9, A10;

        then x is Object of A2 by A3, A12, A11;

        hence thesis;

      end;

      for C1,C2 be lattice-wise category st the carrier of C1 = the carrier of A1 & (for a,b be Object of C1, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f]) & the carrier of C2 = the carrier of A1 & (for a,b be Object of C2, f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[a, b, f]) holds the AltCatStr of C1 = the AltCatStr of C2 from CLCatUniq1;

      hence thesis by A2, A4;

    end;

    scheme :: YELLOW21:sch6

    CLCovariantFunctorEx { P,Q[ set, set, set], A,B() -> lattice-wise category , O( set) -> LATTICE , F( set, set, set) -> Function } :

ex F be covariant strict Functor of A(), B() st (for a be Object of A() holds (F . a) = O(latt)) & for a,b be Object of A() st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = F(latt,latt,@)

      provided

       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]

       and

       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]

       and

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

       and

       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(a), O(b) & Q[O(a), O(b), F(a,b,f)]

       and

       A5: for a be LATTICE st a in the carrier of A() holds F(a,a,id) = ( id O(a))

       and

       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(b,c,g) * F(a,b,f));

      

       A7: for a,b be Object of A() st <^a, b^> <> {} holds for f be Morphism of a, b holds F(a,b,f) in (the Arrows of B() . (O(a),O(b)))

      proof

        let a,b be Object of A() such that

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

        let f be Morphism of a, b;

        

         A9: f = ( @ f) by A8, Def7;

        then P[a, b, f] by A1, A8;

        then

         A10: F(a,b,f) is Function of O(a), O(b) & Q[O(a), O(b), F(a,b,f)] by A4, A9;

        O(a) in the carrier of B() & O(b) in the carrier of B() by A3, A9;

        hence thesis by A2, A10;

      end;

       A11:

      now

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

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

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

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

        let a9,b9,c9 be Object of B() such that

         A14: a9 = O(a) and

         A15: b9 = O(b) and

         A16: c9 = O(c);

        let f9 be Morphism of a9, b9, g9 be Morphism of b9, c9 such that

         A17: f9 = F(a,b,f) & g9 = F(b,c,g);

        

         A18: F(a,b,f) in (the Arrows of B() . (O(a),O(b))) by A7, A12;

        then

         A19: ( @ f9) = f9 by A14, A15, Def7;

        

         A20: ( @ g) = g by A13, Def7;

        then

         A21: P[b, c, g] by A1, A13;

        

         A22: F(b,c,g) in (the Arrows of B() . (O(b),O(c))) by A7, A13;

        then

         A23: ( @ g9) = g9 by A15, A16, Def7;

        

         A24: ( @ f) = f by A12, Def7;

        then P[a, b, f] by A1, A12;

        

        then F(a,c,*) = (F(b,c,g) * F(a,b,f)) by A6, A24, A20, A21

        .= (g9 * f9) by A14, A15, A16, A17, A18, A22, A19, A23, Th3;

        hence F(a,c,*) = (g9 * f9) by A12, A13, Th3;

      end;

       A25:

      now

        let a be Object of A(), a9 be Object of B();

        assume

         A26: a9 = O(a);

        ( idm a) = ( id ( latt a)) by Th2;

        

        hence F(a,a,idm) = ( id ( latt a9)) by A5, A26

        .= ( idm a9) by Th2;

      end;

      

       A27: for a be Object of A() holds O(a) is Object of B()

      proof

        let a be Object of A();

        a is LATTICE by Def4;

        hence thesis by A3;

      end;

      consider F be covariant strict Functor of A(), B() such that

       A28: for a be Object of A() holds (F . a) = O(a) and

       A29: 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) from YELLOW18:sch 8( A27, A7, A11, A25);

      take F;

      thus for a be Object of A() holds (F . a) = O(latt) by A28;

      let a,b be Object of A() such that

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

      let f be Morphism of a, b;

      f = ( @ f) by A30, Def7;

      hence thesis by A29, A30;

    end;

    scheme :: YELLOW21:sch7

    CLContravariantFunctorEx { P,Q[ set, set, set], A,B() -> lattice-wise category , O( set) -> LATTICE , F( set, set, set) -> Function } :

ex F be contravariant strict Functor of A(), B() st (for a be Object of A() holds (F . a) = O(latt)) & for a,b be Object of A() st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = F(latt,latt,@)

      provided

       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]

       and

       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]

       and

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

       and

       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)]

       and

       A5: for a be LATTICE st a in the carrier of A() holds F(a,a,id) = ( id O(a))

       and

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

      

       A7: for a,b be Object of A() st <^a, b^> <> {} holds for f be Morphism of a, b holds F(a,b,f) in (the Arrows of B() . (O(b),O(a)))

      proof

        let a,b be Object of A() such that

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

        let f be Morphism of a, b;

        

         A9: f = ( @ f) by A8, Def7;

        then P[a, b, f] by A1, A8;

        then

         A10: F(a,b,f) is Function of O(b), O(a) & Q[O(b), O(a), F(a,b,f)] by A4, A9;

        O(a) in the carrier of B() & O(b) in the carrier of B() by A3, A9;

        hence thesis by A2, A10;

      end;

       A11:

      now

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

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

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

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

        let a9,b9,c9 be Object of B() such that

         A14: a9 = O(a) and

         A15: b9 = O(b) and

         A16: c9 = O(c);

        let f9 be Morphism of b9, a9, g9 be Morphism of c9, b9 such that

         A17: f9 = F(a,b,f) & g9 = F(b,c,g);

        

         A18: F(a,b,f) in (the Arrows of B() . (O(b),O(a))) by A7, A12;

        then

         A19: ( @ f9) = f9 by A14, A15, Def7;

        

         A20: ( @ g) = g by A13, Def7;

        then

         A21: P[b, c, g] by A1, A13;

        

         A22: F(b,c,g) in (the Arrows of B() . (O(c),O(b))) by A7, A13;

        then

         A23: ( @ g9) = g9 by A15, A16, Def7;

        

         A24: ( @ f) = f by A12, Def7;

        then P[a, b, f] by A1, A12;

        

        then F(a,c,*) = (F(a,b,f) * F(b,c,g)) by A6, A24, A20, A21

        .= (f9 * g9) by A14, A15, A16, A17, A18, A22, A19, A23, Th3;

        hence F(a,c,*) = (f9 * g9) by A12, A13, Th3;

      end;

       A25:

      now

        let a be Object of A(), a9 be Object of B();

        assume

         A26: a9 = O(a);

        ( idm a) = ( id ( latt a)) by Th2;

        

        hence F(a,a,idm) = ( id ( latt a9)) by A5, A26

        .= ( idm a9) by Th2;

      end;

      

       A27: for a be Object of A() holds O(a) is Object of B()

      proof

        let a be Object of A();

        a is LATTICE by Def4;

        hence thesis by A3;

      end;

      consider F be contravariant strict Functor of A(), B() such that

       A28: for a be Object of A() holds (F . a) = O(a) and

       A29: 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) from YELLOW18:sch 9( A27, A7, A11, A25);

      take F;

      thus for a be Object of A() holds (F . a) = O(latt) by A28;

      let a,b be Object of A() such that

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

      let f be Morphism of a, b;

      f = ( @ f) by A30, Def7;

      hence thesis by A29, A30;

    end;

    scheme :: YELLOW21:sch8

    CLCatIsomorphism { P,Q[ set, set, set], A,B() -> lattice-wise category , O( set) -> LATTICE , F( set, set, set) -> Function } :

(A(),B()) are_isomorphic

      provided

       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]

       and

       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]

       and

       A3: ex F be covariant Functor of A(), B() st (for a be Object of A() holds (F . a) = O(a)) & 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)

       and

       A4: for a,b be LATTICE st a in the carrier of A() & b in the carrier of A() holds O(a) = O(b) implies a = b

       and

       A5: for a,b be LATTICE holds for f,g be Function of a, b st P[a, b, f] & P[a, b, g] holds F(a,b,f) = F(a,b,g) implies f = g

       and

       A6: for a,b be LATTICE, f be Function of a, b st Q[a, b, f] holds ex c,d be LATTICE, g be Function of c, d st c in the carrier of A() & d in the carrier of A() & P[c, d, g] & a = O(c) & b = O(d) & f = F(c,d,g);

      

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

      proof

        let a,b be Object of A();

        a = ( latt a) & b = ( latt b);

        hence thesis by A4;

      end;

       A8:

      now

        let a,b be Object of B() such that

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

        let f be Morphism of a, b;

        

         A10: ( @ f) = f by A9, Def7;

        then Q[( latt a), ( latt b), ( @ f)] by A2, A9;

        then

        consider c,d be LATTICE, g be Function of c, d such that

         A11: c in the carrier of A() & d in the carrier of A() and

         A12: P[c, d, g] and

         A13: ( latt a) = O(c) & ( latt b) = O(d) & ( @ f) = F(c,d,g) by A6;

        reconsider c9 = c, d9 = d as Object of A() by A11;

        g in <^c9, d9^> by A1, A12;

        hence ex c,d be Object of A(), g be Morphism of c, d st a = O(c) & b = O(d) & <^c, d^> <> {} & f = F(c,d,g) by A10, A13;

      end;

      

       A14: for a,b be Object of A() st <^a, b^> <> {} holds for f,g be Morphism of a, b st F(a,b,f) = F(a,b,g) holds f = g

      proof

        let a,b be Object of A() such that

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

        let f,g be Morphism of a, b;

        

         A16: ( @ g) = g by A15, Def7;

        then

         A17: P[( latt a), ( latt b), ( @ g)] by A1, A15;

        

         A18: ( @ f) = f by A15, Def7;

        then P[( latt a), ( latt b), ( @ f)] by A1, A15;

        hence thesis by A5, A18, A16, A17;

      end;

      

       A19: ex F be covariant Functor of A(), B() st (for a be Object of A() holds (F . a) = O(a)) & 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 A3;

      thus thesis from YELLOW18:sch 11( A19, A7, A14, A8);

    end;

    scheme :: YELLOW21:sch9

    CLCatAntiIsomorphism { P,Q[ set, set, set], A,B() -> lattice-wise category , O( set) -> LATTICE , F( set, set, set) -> Function } :

(A(),B()) are_anti-isomorphic

      provided

       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]

       and

       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]

       and

       A3: ex F be contravariant Functor of A(), B() st (for a be Object of A() holds (F . a) = O(a)) & 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)

       and

       A4: for a,b be LATTICE st a in the carrier of A() & b in the carrier of A() holds O(a) = O(b) implies a = b

       and

       A5: for a,b be LATTICE, f,g be Function of a, b st F(a,b,f) = F(a,b,g) holds f = g

       and

       A6: for a,b be LATTICE, f be Function of a, b st Q[a, b, f] holds ex c,d be LATTICE, g be Function of c, d st c in the carrier of A() & d in the carrier of A() & P[c, d, g] & b = O(c) & a = O(d) & f = F(c,d,g);

      

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

      proof

        let a,b be Object of A();

        a = ( latt a) & b = ( latt b);

        hence thesis by A4;

      end;

       A8:

      now

        let a,b be Object of B() such that

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

        let f be Morphism of a, b;

        

         A10: ( @ f) = f by A9, Def7;

        then Q[( latt a), ( latt b), ( @ f)] by A2, A9;

        then

        consider c,d be LATTICE, g be Function of c, d such that

         A11: c in the carrier of A() & d in the carrier of A() and

         A12: P[c, d, g] and

         A13: ( latt b) = O(c) & ( latt a) = O(d) & ( @ f) = F(c,d,g) by A6;

        reconsider c9 = c, d9 = d as Object of A() by A11;

        g in <^c9, d9^> by A1, A12;

        hence ex c,d be Object of A(), g be Morphism of c, d st b = O(c) & a = O(d) & <^c, d^> <> {} & f = F(c,d,g) by A10, A13;

      end;

      

       A14: for a,b be Object of A() st <^a, b^> <> {} holds for f,g be Morphism of a, b st F(a,b,f) = F(a,b,g) holds f = g

      proof

        let a,b be Object of A() such that

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

        let f,g be Morphism of a, b;

        ( @ f) = f & ( @ g) = g by A15, Def7;

        hence thesis by A5;

      end;

      

       A16: ex F be contravariant Functor of A(), B() st (for a be Object of A() holds (F . a) = O(a)) & 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 A3;

      thus thesis from YELLOW18:sch 13( A16, A7, A14, A8);

    end;

    begin

    definition

      let C be lattice-wise category;

      :: YELLOW21:def8

      attr C is with_all_isomorphisms means

      : Def8: for a,b be Object of C, f be Function of ( latt a), ( latt b) st f is isomorphic holds f in <^a, b^>;

    end

    registration

      cluster with_all_isomorphisms for strict lattice-wise category;

      existence

      proof

        defpred P[ set, set, set] means $3 = $3;

        set L = the LATTICE;

        

         A1: for a,b,c be LATTICE st a in {L} & b in {L} & c in {L} 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)];

        

         A2: for a be LATTICE st a in {L} holds P[a, a, ( id a)];

        

         A3: for a be Element of {L} holds a is LATTICE by TARSKI:def 1;

        consider C be strict category such that

         A4: C is lattice-wise and

         A5: the carrier of C = {L} & for a,b be LATTICE, f be monotone Function of a, b holds f in (the Arrows of C . (a,b)) iff a in {L} & b in {L} & P[a, b, f] from localCLCatEx( A3, A1, A2);

        reconsider C as strict lattice-wise category by A4;

        take C;

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

        thus thesis by A5;

      end;

    end

    theorem :: YELLOW21:4

    for C be with_all_isomorphisms lattice-wise category holds for a,b be Object of C holds for f be Morphism of a, b st ( @ f) is isomorphic holds f is iso

    proof

      let C be with_all_isomorphisms lattice-wise category;

      let a,b be Object of C;

      let f be Morphism of a, b;

      assume

       A1: ( @ f) is isomorphic;

      then

      consider g be monotone Function of ( latt b), ( latt a) such that

       A2: (( @ f) * g) = ( id ( latt b)) and

       A3: (g * ( @ f)) = ( id ( latt a)) by YELLOW16: 15;

      

       A4: ( @ f) in <^a, b^> by A1, Def8;

      

       A5: g is isomorphic by A2, A3, YELLOW16: 15;

      then

       A6: g in <^b, a^> by Def8;

      reconsider g as Morphism of b, a by A5, Def8;

      

       A7: ( @ g) = g by A6, Def7;

      ( idm b) = ( id ( latt b)) by Th2;

      then (f * g) = ( idm b) by A2, A4, A6, A7, Th3;

      then

       A8: g is_right_inverse_of f;

      ( idm a) = ( id ( latt a)) by Th2;

      then (g * f) = ( idm a) by A3, A4, A6, A7, Th3;

      then

       A9: g is_left_inverse_of f;

      then f is retraction coretraction by A8;

      hence (f * (f " )) = ( idm b) & ((f " ) * f) = ( idm a) by A4, A6, A9, A8, ALTCAT_3:def 4;

    end;

    theorem :: YELLOW21:5

    for C be lattice-wise category holds for a,b be Object of C st <^a, b^> <> {} & <^b, a^> <> {} holds for f be Morphism of a, b st f is iso holds ( @ f) is isomorphic

    proof

      let C be lattice-wise category;

      let a,b be Object of C;

      assume

       A1: <^a, b^> <> {} & <^b, a^> <> {} ;

      let f be Morphism of a, b such that

       A2: (f * (f " )) = ( idm b) & ((f " ) * f) = ( idm a);

      

       A3: ( idm a) = ( id ( latt a)) & ( idm b) = ( id ( latt b)) by Th2;

      (( @ f) * ( @ (f " ))) = (f * (f " )) & (( @ (f " )) * ( @ f)) = ((f " ) * f) by A1, Th3;

      hence thesis by A2, A3, YELLOW16: 15;

    end;

    scheme :: YELLOW21:sch10

    CLCatEquivalence { P,Q[ set, set, set], A,B() -> lattice-wise category , O1,O2( set) -> LATTICE , F1,F2( set, set, set) -> Function , A,B( set) -> Function } :

(A(),B()) are_equivalent

      provided

       A1: for a,b be Object of A(), f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff P[( latt a), ( latt b), f]

       and

       A2: for a,b be Object of B(), f be monotone Function of ( latt a), ( latt b) holds f in <^a, b^> iff Q[( latt a), ( latt b), f]

       and

       A3: ex F be covariant Functor of A(), B() st (for a be Object of A() holds (F . a) = O1(a)) & for a,b be Object of A() st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = F1(a,b,f)

       and

       A4: ex G be covariant Functor of B(), A() st (for a be Object of B() holds (G . a) = O2(a)) & for a,b be Object of B() st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . f) = F2(a,b,f)

       and

       A5: for a be LATTICE st a in the carrier of A() holds ex f be monotone Function of O2(O1), a st f = A(a) & f is isomorphic & P[O2(O1), a, f] & P[a, O2(O1), (f " )]

       and

       A6: for a be LATTICE st a in the carrier of B() holds ex f be monotone Function of a, O1(O2) st f = B(a) & f is isomorphic & Q[a, O1(O2), f] & Q[O1(O2), a, (f " )]

       and

       A7: for a,b be Object of A() st <^a, b^> <> {} holds for f be Morphism of a, b holds (A(b) * F2(O1,O1,F1)) = (( @ f) * A(a))

       and

       A8: for a,b be Object of B() st <^a, b^> <> {} holds for f be Morphism of a, b holds (F1(O2,O2,F2) * B(a)) = (B(b) * ( @ f));

      

       A9: ex G be covariant Functor of B(), A() st (for a be Object of B() holds (G . a) = O2(a)) & for a,b be Object of B() st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . f) = F2(a,b,f) by A4;

      

       A10: for a,b be Object of B() st <^a, b^> <> {} holds for f be Morphism of a, b holds (F1(O2,O2,F2) * B(a)) = (B(b) * f)

      proof

        let a,b be Object of B() such that

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

        let f be Morphism of a, b;

        ( @ f) = f by A11, Def7;

        hence thesis by A8, A11;

      end;

      

       A12: for a,b be Object of A() st <^a, b^> <> {} holds for f be Morphism of a, b holds (A(b) * F2(O1,O1,F1)) = (f * A(a))

      proof

        let a,b be Object of A() such that

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

        let f be Morphism of a, b;

        ( @ f) = f by A13, Def7;

        hence thesis by A7, A13;

      end;

      

       A14: for a,b be Object of B() st b = O1(O2) holds B(a) in <^a, b^> & (B(a) " ) in <^b, a^> & B(a) is one-to-one

      proof

        let a,b be Object of B() such that

         A15: b = O1(O2);

        consider f be monotone Function of ( latt a), O1(O2) such that

         A16: f = B(a) and

         A17: f is isomorphic and

         A18: Q[( latt a), O1(O2), f] and

         A19: Q[O1(O2), ( latt a), (f " )] by A6;

        

         A20: ( latt b) = b;

        hence B(a) in <^a, b^> by A2, A15, A16, A18;

        ex g be Function of O1(O2), ( latt a) st g = (f " ) & g is monotone by A17, WAYBEL_0:def 38;

        hence (B(a) " ) in <^b, a^> by A2, A15, A20, A16, A19;

        thus thesis by A16, A17;

      end;

      

       A21: for a,b be Object of A() st a = O2(O1) holds A(b) in <^a, b^> & (A(b) " ) in <^b, a^> & A(b) is one-to-one

      proof

        let a,b be Object of A() such that

         A22: a = O2(O1);

        consider f be monotone Function of O2(O1), ( latt b) such that

         A23: f = A(b) and

         A24: f is isomorphic and

         A25: P[O2(O1), ( latt b), f] and

         A26: P[( latt b), O2(O1), (f " )] by A5;

        

         A27: ( latt a) = a;

        hence A(b) in <^a, b^> by A1, A22, A23, A25;

        ex g be Function of ( latt b), O2(O1) st g = (f " ) & g is monotone by A24, WAYBEL_0:def 38;

        hence (A(b) " ) in <^b, a^> by A1, A22, A27, A23, A26;

        thus thesis by A23, A24;

      end;

      

       A28: ex F be covariant Functor of A(), B() st (for a be Object of A() holds (F . a) = O1(a)) & for a,b be Object of A() st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . f) = F1(a,b,f) by A3;

      thus thesis from YELLOW18:sch 22( A28, A9, A21, A14, A12, A10);

    end;

    begin

    definition

      let R be Relation;

      :: YELLOW21:def9

      attr R is upper-bounded means ex x st for y st y in ( field R) holds [y, x] in R;

    end

    

     Lm1: for X be set holds x in X iff X = ((X \ {x}) \/ {x}) by ZFMISC_1: 31, XBOOLE_1: 7, XBOOLE_1: 45;

    registration

      cluster well-ordering -> reflexive transitive antisymmetric connected well_founded for Relation;

      coherence ;

    end

    registration

      cluster well-ordering for Relation;

      existence

      proof

        consider r be Relation such that

         A1: r well_orders { 0 , 1, 2, 3, 4} by WELLORD2: 17;

        take (r |_2 { 0 , 1, 2, 3, 4});

        thus thesis by A1, WELLORD2: 16;

      end;

    end

    theorem :: YELLOW21:6

    

     Th6: for x,y be object holds for f be one-to-one Function, R be Relation holds [x, y] in ((f * R) * (f " )) iff x in ( dom f) & y in ( dom f) & [(f . x), (f . y)] in R

    proof

      let x,y be object;

      let f be one-to-one Function, R be Relation;

      

       A1: ( rng f) = ( dom (f " )) by FUNCT_1: 33;

      

       A2: ( dom f) = ( rng (f " )) by FUNCT_1: 33;

      hereby

        assume [x, y] in ((f * R) * (f " ));

        then

        consider a be object such that

         A3: [x, a] in (f * R) and

         A4: [a, y] in (f " ) by RELAT_1:def 8;

        

         A5: y = ((f " ) . a) & a in ( rng f) by A1, A4, FUNCT_1: 1;

        consider b be object such that

         A6: [x, b] in f and

         A7: [b, a] in R by A3, RELAT_1:def 8;

        thus x in ( dom f) & y in ( dom f) by A2, A4, A6, XTUPLE_0:def 12, XTUPLE_0:def 13;

        b = (f . x) by A6, FUNCT_1: 1;

        hence [(f . x), (f . y)] in R by A7, A5, FUNCT_1: 35;

      end;

      assume that

       A8: x in ( dom f) and

       A9: y in ( dom f) and

       A10: [(f . x), (f . y)] in R;

      ((f " ) . (f . y)) = y & (f . y) in ( rng f) by A9, FUNCT_1: 34, FUNCT_1:def 3;

      then

       A11: [(f . y), y] in (f " ) by A1, FUNCT_1: 1;

       [x, (f . x)] in f by A8, FUNCT_1: 1;

      then [x, (f . y)] in (f * R) by A10, RELAT_1:def 8;

      hence thesis by A11, RELAT_1:def 8;

    end;

    registration

      let f be one-to-one Function;

      let R be reflexive Relation;

      cluster ((f * R) * (f " )) -> reflexive;

      coherence

      proof

        let x be object;

        

         A1: R is_reflexive_in ( field R) by RELAT_2:def 9;

        assume x in ( field ((f * R) * (f " )));

        then

         A2: x in (( dom ((f * R) * (f " ))) \/ ( rng ((f * R) * (f " )))) by RELAT_1:def 6;

        per cases by A2, XBOOLE_0:def 3;

          suppose x in ( dom ((f * R) * (f " )));

          then

          consider y be object such that

           A3: [x, y] in ((f * R) * (f " )) by XTUPLE_0:def 12;

           [(f . x), (f . y)] in R by A3, Th6;

          then (f . x) in ( field R) by RELAT_1: 15;

          then

           A4: [(f . x), (f . x)] in R by A1;

          x in ( dom f) by A3, Th6;

          hence thesis by A4, Th6;

        end;

          suppose x in ( rng ((f * R) * (f " )));

          then

          consider y be object such that

           A5: [y, x] in ((f * R) * (f " )) by XTUPLE_0:def 13;

           [(f . y), (f . x)] in R by A5, Th6;

          then (f . x) in ( field R) by RELAT_1: 15;

          then

           A6: [(f . x), (f . x)] in R by A1;

          x in ( dom f) by A5, Th6;

          hence thesis by A6, Th6;

        end;

      end;

    end

    registration

      let f be one-to-one Function;

      let R be antisymmetric Relation;

      cluster ((f * R) * (f " )) -> antisymmetric;

      coherence

      proof

        let x,y be object;

        assume that x in ( field ((f * R) * (f " ))) and y in ( field ((f * R) * (f " )));

        assume that

         A1: [x, y] in ((f * R) * (f " )) and

         A2: [y, x] in ((f * R) * (f " ));

        

         A3: x in ( dom f) & y in ( dom f) by A1, Th6;

        

         A4: R is_antisymmetric_in ( field R) by RELAT_2:def 12;

        

         A5: [(f . y), (f . x)] in R by A2, Th6;

        

         A6: [(f . x), (f . y)] in R by A1, Th6;

        then (f . x) in ( field R) & (f . y) in ( field R) by RELAT_1: 15;

        then (f . x) = (f . y) by A6, A5, A4;

        hence thesis by A3, FUNCT_1:def 4;

      end;

    end

    registration

      let f be one-to-one Function;

      let R be transitive Relation;

      cluster ((f * R) * (f " )) -> transitive;

      coherence

      proof

        let x,y,z be object;

        assume that x in ( field ((f * R) * (f " ))) and y in ( field ((f * R) * (f " ))) and z in ( field ((f * R) * (f " )));

        assume that

         A1: [x, y] in ((f * R) * (f " )) and

         A2: [y, z] in ((f * R) * (f " ));

        

         A3: x in ( dom f) & z in ( dom f) by A1, A2, Th6;

        

         A4: [(f . y), (f . z)] in R by A2, Th6;

        then

         A5: (f . z) in ( field R) by RELAT_1: 15;

        

         A6: R is_transitive_in ( field R) by RELAT_2:def 16;

        

         A7: [(f . x), (f . y)] in R by A1, Th6;

        then (f . x) in ( field R) & (f . y) in ( field R) by RELAT_1: 15;

        then [(f . x), (f . z)] in R by A7, A4, A5, A6;

        hence thesis by A3, Th6;

      end;

    end

    theorem :: YELLOW21:7

    

     Th7: for X be set, A be Ordinal st (X,A) are_equipotent holds ex R be Order of X st R well_orders X & ( order_type_of R) = A

    proof

      let X be set, A be Ordinal;

      given f be Function such that

       A1: f is one-to-one and

       A2: ( dom f) = X and

       A3: ( rng f) = A;

      reconsider f as Function of X, A by A2, A3, FUNCT_2: 2;

      reconsider g = (f " ) as Function of A, X by A1, A3, FUNCT_2: 25;

      

       A4: ( dom g) = A by A1, A3, FUNCT_1: 33;

      reconsider f9 = f as one-to-one Function by A1;

      

       A5: ( dom ( RelIncl A)) = A by ORDERS_1: 14;

      ( rng ( RelIncl A)) = A by ORDERS_1: 14;

      then

       A6: ( rng (f * ( RelIncl A))) = A by A3, A5, RELAT_1: 28;

      set R = ((f * ( RelIncl A)) * g);

      ( dom (f * ( RelIncl A))) = X by A2, A3, A5, RELAT_1: 27;

      then

       A7: ( dom R) = X by A4, A6, RELAT_1: 27;

      ( rng g) = X by A1, A2, FUNCT_1: 33;

      then ( rng R) = X by A4, A6, RELAT_1: 28;

      

      then

       A8: ( field R) = (X \/ X) by A7, RELAT_1:def 6

      .= X;

      reconsider R as Relation of X;

      ((f9 * ( RelIncl A)) * (f9 " )) is_reflexive_in X by A8, RELAT_2:def 9;

      then

      reconsider R as Order of X by A7, PARTFUN1:def 2;

      

       A9: f is_isomorphism_of (R,( RelIncl A))

      proof

        thus ( dom f) = ( field R) & ( rng f) = ( field ( RelIncl A)) & f is one-to-one by A1, A2, A3, A8, WELLORD2:def 1;

        let a,b be object;

        hereby

          assume

           A10: [a, b] in R;

          hence a in ( field R) & b in ( field R) by RELAT_1: 15;

          consider x be object such that

           A11: [a, x] in (f * ( RelIncl A)) and

           A12: [x, b] in g by A10, RELAT_1:def 8;

          

           A13: b = (g . x) & x in ( dom g) by A12, FUNCT_1: 1;

          consider y be object such that

           A14: [a, y] in f and

           A15: [y, x] in ( RelIncl A) by A11, RELAT_1:def 8;

          y = (f . a) by A14, FUNCT_1: 1;

          hence [(f . a), (f . b)] in ( RelIncl A) by A1, A3, A15, A13, FUNCT_1: 35;

        end;

        assume that

         A16: a in ( field R) and

         A17: b in ( field R) and

         A18: [(f . a), (f . b)] in ( RelIncl A);

         [a, (f . a)] in f by A2, A8, A16, FUNCT_1: 1;

        then

         A19: [a, (f . b)] in (f * ( RelIncl A)) by A18, RELAT_1:def 8;

        ((f " ) . (f . b)) = b & (f . b) in A by A1, A2, A3, A8, A17, FUNCT_1: 34, FUNCT_1:def 3;

        then [(f . b), b] in g by A4, FUNCT_1: 1;

        hence thesis by A19, RELAT_1:def 8;

      end;

      then (f " ) is_isomorphism_of (( RelIncl A),R) by WELLORD1: 39;

      then R is connected well_founded by WELLORD1: 43;

      then

       A20: R is_connected_in X & R is_well_founded_in X by A8;

      take R;

      

       A21: R is_antisymmetric_in X by A8, RELAT_2:def 12;

      R is_reflexive_in X & R is_transitive_in X by A8, RELAT_2:def 9, RELAT_2:def 16;

      hence R well_orders X by A21, A20;

      then

       A22: R is well-ordering by A8, WELLORD1: 4;

      (R,( RelIncl A)) are_isomorphic by A9;

      hence thesis by A22, WELLORD2:def 2;

    end;

    registration

      let X be non empty set;

      cluster upper-bounded well-ordering for Order of X;

      existence

      proof

        set x = the Element of X;

        

         A1: ((X \ {x}),( card (X \ {x}))) are_equipotent & ( {x}, {( card (X \ {x}))}) are_equipotent by CARD_1: 28, CARD_1:def 2;

        

         A2: ( succ ( card (X \ {x}))) = (( card (X \ {x})) \/ {( card (X \ {x}))}) by ORDINAL1:def 1;

         not ( card (X \ {x})) in ( card (X \ {x}));

        then

         A3: {( card (X \ {x}))} misses ( card (X \ {x})) by ZFMISC_1: 50;

         {x} misses (X \ {x}) & X = ((X \ {x}) \/ {x}) by Lm1, XBOOLE_1: 79;

        then

        consider r be Order of X such that

         A4: r well_orders X and

         A5: ( order_type_of r) = ( succ ( card (X \ {x}))) by A1, A3, A2, Th7, CARD_1: 31;

        take r;

        

         A6: ( field r) = X by ORDERS_1: 15;

        then r is well-ordering by A4, WELLORD1: 4;

        then (r,( RelIncl ( order_type_of r))) are_isomorphic by WELLORD2:def 2;

        then (( RelIncl ( order_type_of r)),r) are_isomorphic by WELLORD1: 40;

        then

        consider f be Function such that

         A7: f is_isomorphism_of (( RelIncl ( order_type_of r)),r);

        

         A8: f is one-to-one by A7;

        

         A9: ( rng f) = X by A6, A7;

        ( field ( RelIncl ( order_type_of r))) = ( order_type_of r) by WELLORD2:def 1;

        then

         A10: ( dom f) = ( order_type_of r) by A7;

        thus r is upper-bounded

        proof

          take a = (f . ( card (X \ {x})));

          let y;

          

           A11: ( card (X \ {x})) in ( order_type_of r) by A2, A5, ZFMISC_1: 136;

          assume

           A12: y in ( field r);

          then

           A13: ((f " ) . y) in ( order_type_of r) by A6, A8, A10, A9, FUNCT_1: 32;

          then

          reconsider b = ((f " ) . y) as Ordinal;

          ((f " ) . y) in ( card (X \ {x})) or ((f " ) . y) = ( card (X \ {x})) by A2, A5, A13, ZFMISC_1: 136;

          then b c= ( card (X \ {x})) by ORDINAL1:def 2;

          then [b, ( card (X \ {x}))] in ( RelIncl ( order_type_of r)) by A13, A11, WELLORD2:def 1;

          then [(f . b), a] in r by A7;

          hence thesis by A6, A8, A9, A12, FUNCT_1: 35;

        end;

        thus thesis by A4, A6, WELLORD1: 4;

      end;

    end

    theorem :: YELLOW21:8

    

     Th8: for P be reflexive non empty RelStr holds P is upper-bounded iff the InternalRel of P is upper-bounded

    proof

      let P be reflexive non empty RelStr;

      (the carrier of P \/ the carrier of P) = the carrier of P;

      then

       A1: ( field the InternalRel of P) c= the carrier of P by RELSET_1: 8;

      thus P is upper-bounded implies the InternalRel of P is upper-bounded

      proof

        given x be Element of P such that

         A2: x is_>=_than the carrier of P;

        take x;

        let y;

        assume y in ( field the InternalRel of P);

        then

        reconsider y as Element of P by A1;

        x >= y by A2;

        hence thesis;

      end;

      set y = the Element of P;

      given x such that

       A3: for y st y in ( field the InternalRel of P) holds [y, x] in the InternalRel of P;

      y <= y;

      then [y, y] in the InternalRel of P;

      then y in ( field the InternalRel of P) by RELAT_1: 15;

      then [y, x] in the InternalRel of P by A3;

      then x in ( field the InternalRel of P) by RELAT_1: 15;

      then

      reconsider x as Element of P by A1;

      take x;

      let y be Element of P;

      y <= y;

      then [y, y] in the InternalRel of P;

      then y in ( field the InternalRel of P) by RELAT_1: 15;

      then [y, x] in the InternalRel of P by A3;

      hence thesis;

    end;

    theorem :: YELLOW21:9

    

     Th9: for P be upper-bounded non empty Poset st the InternalRel of P is well-ordering holds P is connected complete continuous

    proof

      let P be upper-bounded non empty Poset such that

       A1: the InternalRel of P is well-ordering;

      

       A2: ( field the InternalRel of P) = the carrier of P by ORDERS_1: 15;

      thus

       A3: P is connected

      proof

        let x,y be Element of P;

        

         A4: x = y or x <> y;

        the InternalRel of P is_connected_in the carrier of P & the InternalRel of P is_reflexive_in the carrier of P by A1, A2, RELAT_2:def 9, RELAT_2:def 14;

        then [x, y] in the InternalRel of P or [y, x] in the InternalRel of P by A4;

        hence x <= y or y <= x;

      end;

      thus P is complete

      proof

        set y = the Element of P;

        let X be set;

        defpred P[ object] means for y be Element of P st y in X holds [y, $1] in the InternalRel of P;

        consider Y be set such that

         A5: for x be object holds x in Y iff x in the carrier of P & P[x] from XBOOLE_0:sch 1;

        

         A6: Y c= the carrier of P by A5;

        the InternalRel of P is upper-bounded by Th8;

        then

        consider x such that

         A7: for y st y in ( field the InternalRel of P) holds [y, x] in the InternalRel of P;

         [y, x] in the InternalRel of P by A2, A7;

        then

        reconsider x as Element of P by A2, RELAT_1: 15;

        for y be Element of P st y in X holds [y, x] in the InternalRel of P by A2, A7;

        then x in Y by A5;

        then

        consider a be object such that

         A8: a in Y and

         A9: for b be object st b in Y holds [a, b] in the InternalRel of P by A1, A2, A6, WELLORD1: 6;

        reconsider a as Element of P by A6, A8;

        take a;

        thus for y be Element of P st y in X holds y <= a by A5, A8;

        let b be Element of P;

        assume

         A10: for c be Element of P st c in X holds c <= b;

        for c be Element of P st c in X holds [c, b] in the InternalRel of P by ORDERS_2:def 5, A10;

        then b in Y by A5;

        then [a, b] in the InternalRel of P by A9;

        hence a <= b;

      end;

      hence thesis by A3;

    end;

    theorem :: YELLOW21:10

    

     Th10: for P be upper-bounded non empty Poset st the InternalRel of P is well-ordering holds for x,y be Element of P st y < x holds ex z be Element of P st z is compact & y <= z & z <= x

    proof

      let P be upper-bounded non empty Poset;

      set R = the InternalRel of P, A = ( order_type_of R);

      

       A1: ( field ( RelIncl A)) = A by WELLORD2:def 1;

      assume

       A2: R is well-ordering;

      then

      reconsider L = P as complete Chain by Th9;

      let x,y be Element of P;

      (R,( RelIncl A)) are_isomorphic by A2, WELLORD2:def 2;

      then

      consider f be Function such that

       A3: f is_isomorphism_of (R,( RelIncl A));

      assume

       A4: y < x;

      then y <= x;

      then

       A5: [y, x] in R;

      then

       A6: [(f . y), (f . x)] in ( RelIncl A) by A3;

      then

       A7: (f . x) in A by A1, RELAT_1: 15;

      

       A8: (f . x) <> (f . y) by A3, A4, A5, WELLORD1: 36;

      

       A9: (f . y) in A by A6, A1, RELAT_1: 15;

      then

      reconsider a = (f . x), b = (f . y) as Ordinal by A7;

      b c= a by A6, A7, A9, WELLORD2:def 1;

      then b c< a by A8;

      then b in a by ORDINAL1: 11;

      then

       A10: ( succ b) c= a by ORDINAL1: 21;

      then

       A11: ( succ b) in A by A7, ORDINAL1: 12;

      then

       A12: [( succ b), (f . x)] in ( RelIncl A) by A7, A10, WELLORD2:def 1;

      

       A13: b c= ( succ b) by ORDINAL3: 1;

      ( rng f) = A by A3, A1;

      then

      consider z be object such that

       A14: z in ( dom f) and

       A15: ( succ b) = (f . z) by A11, FUNCT_1:def 3;

      

       A16: ( field R) = the carrier of P by ORDERS_1: 15;

      then

      reconsider z as Element of P by A3, A14;

      take z;

      

       A17: ( dom f) = ( field R) by A3;

      thus z is compact

      proof

        let D be non empty directed Subset of P such that

         A18: z <= ( sup D) and

         A19: for d be Element of P st d in D holds not z <= d;

        

         A20: L is complete;

        D is_<=_than y

        proof

          let c be Element of P;

          

           A21: f is one-to-one by A3;

          assume

           A22: c in D;

          then not z <= c by A19;

          then z >= c by A20, WAYBEL_0:def 29;

          then [c, z] in R;

          then

           A23: [(f . c), ( succ b)] in ( RelIncl A) by A3, A15;

          then

           A24: (f . c) in A by A1, RELAT_1: 15;

          then

          reconsider fc = (f . c) as Ordinal;

          

           A25: fc c= ( succ b) by A11, A23, A24, WELLORD2:def 1;

          c <> z by A19, A22;

          then fc <> ( succ b) by A15, A16, A17, A21, FUNCT_1:def 4;

          then fc c< ( succ b) by A25;

          then fc in ( succ b) by ORDINAL1: 11;

          then fc c= b by ORDINAL1: 22;

          then [fc, b] in ( RelIncl A) by A9, A24, WELLORD2:def 1;

          hence [c, y] in R by A3, A16;

        end;

        then ( sup D) <= y by A20, YELLOW_0: 32;

        then z <= y by A18, YELLOW_0:def 2;

        then [z, y] in R;

        then [( succ b), b] in ( RelIncl A) by A3, A15;

        then ( succ b) c= b by A9, A11, WELLORD2:def 1;

        then b = ( succ b) by A13;

        hence contradiction by ORDINAL1: 9;

      end;

       [(f . y), ( succ b)] in ( RelIncl A) by A9, A13, A11, WELLORD2:def 1;

      hence [y, z] in R & [z, x] in R by A3, A15, A16, A12;

    end;

    theorem :: YELLOW21:11

    

     Th11: for P be upper-bounded non empty Poset st the InternalRel of P is well-ordering holds P is algebraic

    proof

      let P be upper-bounded non empty Poset;

      assume

       A1: the InternalRel of P is well-ordering;

      then

      reconsider L = P as connected complete continuous non empty Poset by Th9;

      now

        let x,y be Element of L;

        assume x << y;

        then x is compact & x <= x & x <= y or x < y by WAYBEL_3: 1;

        then

        consider z be Element of L such that

         A2: z is compact and

         A3: x <= z & z <= y by A1, Th10;

        take z;

        thus z in the carrier of ( CompactSublatt L) by A2, WAYBEL_8:def 1;

        thus x <= z & z <= y by A3;

      end;

      hence thesis by WAYBEL_8: 7;

    end;

    registration

      let X be non empty set;

      let R be upper-bounded well-ordering Order of X;

      cluster RelStr (# X, R #) -> complete connected continuous algebraic;

      coherence

      proof

         RelStr (# X, R #) is upper-bounded by Th8;

        hence thesis by Th9, Th11;

      end;

    end

    definition

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

      defpred L[ LATTICE] means $1 is complete;

      let W be non empty set;

      given w be Element of W such that

       A1: w is non empty;

      :: YELLOW21:def10

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

      : Def10: (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 directed-sups-preserving;

      existence

      proof

        reconsider w as non empty set by A1;

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

        

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

         RelStr (# w, r #) is complete;

        then

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

        

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

        thus ex It be lattice-wise strict category st (for x be LATTICE holds x is Object of It iff x is strict & L[x] & 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 P[( latt a), ( latt b), f] from CLCatEx2( A3, A4, A2);

      end;

      correctness

      proof

        reconsider w as non empty set by A1;

        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 directed-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 directed-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 directed-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 directed-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 directed-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 CLCatUniq2;

        hence thesis by A5, A7, A9, A10;

      end;

    end

    registration

      let W be with_non-empty_element set;

      cluster (W -UPS_category ) -> with_complete_lattices with_all_isomorphisms;

      coherence

      proof

        set C = (W -UPS_category );

        thus C is lattice-wise;

        

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

        hereby

          let a be Object of C;

          a = ( latt a);

          hence a is complete LATTICE by A1, Def10;

        end;

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

        reconsider S = ( latt a), T = ( latt b) as complete LATTICE by A1, Def10;

        assume f is isomorphic;

        then f is sups-preserving Function of S, T by WAYBEL13: 20;

        hence thesis by A1, Def10;

      end;

    end

    theorem :: YELLOW21:12

    

     Th12: for W be with_non-empty_element set holds the carrier of (W -UPS_category ) c= ( POSETS W)

    proof

      let W be with_non-empty_element set;

      let x be object;

      assume x in the carrier of (W -UPS_category );

      then

      reconsider x as Object of (W -UPS_category );

      

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

      then

       A2: the carrier of ( latt x) in W by Def10;

      ( latt x) = x;

      then x is strict Poset by A1, Def10;

      hence thesis by A2, Def2;

    end;

    theorem :: YELLOW21:13

    

     Th13: for W be with_non-empty_element set holds for x holds x is Object of (W -UPS_category ) iff x is complete LATTICE & x in ( POSETS W)

    proof

      let W be with_non-empty_element set;

      let x;

      hereby

        assume x is Object of (W -UPS_category );

        then

        reconsider a = x as Object of (W -UPS_category );

        ( latt a) = x;

        hence x is complete LATTICE;

        a in the carrier of (W -UPS_category ) & the carrier of (W -UPS_category ) c= ( POSETS W) by Th12;

        hence x in ( POSETS W);

      end;

      assume x is complete LATTICE;

      then

      reconsider L = x as complete LATTICE;

      assume x in ( POSETS W);

      then

       A1: the carrier of (L as_1-sorted ) in W & L is strict by Def2;

      (L as_1-sorted ) = L by Def1;

      hence thesis by A1, Def10;

    end;

    theorem :: YELLOW21:14

    

     Th14: 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 -UPS_category ) iff L is strict complete

    proof

      let W be with_non-empty_element set;

      let L be LATTICE;

      assume

       A1: the carrier of L in W;

      (L as_1-sorted ) = L by Def1;

      then L in ( POSETS W) iff L is strict by A1, Def2;

      hence thesis by Th13;

    end;

    theorem :: YELLOW21:15

    

     Th15: for W be with_non-empty_element set holds for a,b be Object of (W -UPS_category ) holds for f be set holds f in <^a, b^> iff f is 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 -UPS_category );

      let f be set;

      

       A1: ex w be non empty set st w 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, Def7;

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

      end;

      thus thesis by A1, Def10;

    end;

    registration

      let W be with_non-empty_element set;

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

      cluster <^a, b^> -> non empty;

      coherence

      proof

        set f = the directed-sups-preserving Function of ( latt a), ( latt b);

        f in <^a, b^> by Th15;

        hence thesis;

      end;

    end

    begin

    registration

      let A be set-id-inheriting category;

      cluster -> set-id-inheriting for non empty subcategory of A;

      coherence

      proof

        let B be non empty subcategory of A;

        let b be Object of B;

        b in the carrier of B & the carrier of B c= the carrier of A by ALTCAT_2:def 11;

        then

        reconsider a = b as Object of A;

        

        thus ( idm b) = ( idm a) by ALTCAT_2: 34

        .= ( id ( the_carrier_of a)) by YELLOW18:def 10

        .= ( id ( the_carrier_of b)) by ALTCAT_2: 34;

      end;

    end

    registration

      let A be para-functional category;

      cluster -> para-functional for non empty subcategory of A;

      coherence

      proof

        let B be non empty subcategory of A;

        consider F be ManySortedSet of A such that

         A1: for a1,a2 be Object of A holds <^a1, a2^> c= ( Funcs ((F . a1),(F . a2))) by YELLOW18:def 7;

        set G = (F | the carrier of B);

        

         A2: the carrier of B c= the carrier of A by ALTCAT_2:def 11;

        ( dom F) = the carrier of A by PARTFUN1:def 2;

        then ( dom G) = the carrier of B by A2, RELAT_1: 62;

        then

        reconsider G as ManySortedSet of B by PARTFUN1:def 2, RELAT_1:def 18;

        take G;

        let a1,a2 be Object of B;

        reconsider b1 = a1, b2 = a2 as Object of A by A2;

        (F . a1) = (G . a1) & (F . a2) = (G . a2) by FUNCT_1: 49;

        then <^a1, a2^> c= <^b1, b2^> & <^b1, b2^> c= ( Funcs ((G . a1),(G . a2))) by A1, ALTCAT_2: 31;

        hence thesis;

      end;

    end

    registration

      let A be semi-functional category;

      cluster -> semi-functional for non empty transitive SubCatStr of A;

      coherence

      proof

        let B be non empty transitive SubCatStr of A;

        let b1,b2,b3 be Object of B such that

         A1: <^b1, b2^> <> {} and

         A2: <^b2, b3^> <> {} and

         A3: <^b1, b3^> <> {} ;

        reconsider a1 = b1, a2 = b2, a3 = b3 as Object of A by ALTCAT_2: 29;

        

         A4: <^a1, a2^> <> {} & <^a2, a3^> <> {} by A1, A2, ALTCAT_2: 31, XBOOLE_1: 3;

        let f1 be Morphism of b1, b2, f2 be Morphism of b2, b3;

        reconsider g2 = f2 as Morphism of a2, a3 by A2, ALTCAT_2: 33;

        reconsider g1 = f1 as Morphism of a1, a2 by A1, ALTCAT_2: 33;

        

         A5: <^a1, a3^> <> {} by A3, ALTCAT_2: 31, XBOOLE_1: 3;

        let f9,g9 be Function;

        assume f1 = f9 & f2 = g9;

        then (g2 * g1) = (g9 * f9) by A4, A5, ALTCAT_1:def 12;

        hence thesis by A1, A2, ALTCAT_2: 32;

      end;

    end

    registration

      let A be carrier-underlaid category;

      cluster -> carrier-underlaid for non empty subcategory of A;

      coherence

      proof

        let B be non empty subcategory of A;

        let b be Object of B;

        reconsider a = b as Object of A by ALTCAT_2: 29;

        consider S be 1-sorted such that

         A1: a = S and

         A2: ( the_carrier_of a) = the carrier of S by Def3;

        take S;

        thus b = S by A1;

        thus thesis by A2, ALTCAT_2: 34;

      end;

    end

    registration

      let A be lattice-wise category;

      cluster -> lattice-wise for non empty subcategory of A;

      coherence

      proof

        let B be non empty subcategory of A;

        thus B is semi-functional set-id-inheriting;

        hereby

          let b be Object of B;

          reconsider a = b as Object of A by ALTCAT_2: 29;

          a is LATTICE by Def4;

          hence b is LATTICE;

        end;

        let a,b be Object of B;

        reconsider a9 = a, b9 = b as Object of A by ALTCAT_2: 29;

        let A,B be LATTICE;

        assume A = a & B = b;

        then <^a, b^> c= <^a9, b9^> & <^a9, b9^> c= ( MonFuncs (A,B)) by Def4, ALTCAT_2: 31;

        hence thesis;

      end;

    end

    registration

      let A be with_all_isomorphisms lattice-wise category;

      cluster full -> with_all_isomorphisms for non empty subcategory of A;

      coherence

      proof

        let B be non empty subcategory of A such that

         A1: B is full;

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

        reconsider a9 = a, b9 = b as Object of A by ALTCAT_2: 29;

        assume f is isomorphic;

        then f in <^a9, b9^> by Def8;

        hence thesis by A1, ALTCAT_2: 28;

      end;

    end

    registration

      let A be with_complete_lattices category;

      cluster -> with_complete_lattices for non empty subcategory of A;

      coherence

      proof

        let B be non empty subcategory of A;

        thus B is lattice-wise;

        let b be Object of B;

        reconsider a = b as Object of A by ALTCAT_2: 29;

        a is complete LATTICE by Def5;

        hence thesis;

      end;

    end

    definition

      let W be with_non-empty_element set;

      defpred P[ Object of (W -UPS_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 #);

      :: YELLOW21:def11

      func W -CONT_category -> strict full non empty subcategory of (W -UPS_category ) means

      : Def11: for a be Object of (W -UPS_category ) holds a is Object of it iff ( latt a) is continuous;

      existence

      proof

        reconsider b as Object of (W -UPS_category ) by A1, Def10;

        b = ( latt b);

        then

         A2: ex b be Object of (W -UPS_category ) st P[b];

        thus ex C be strict full non empty subcategory of (W -UPS_category ) st for a be Object of (W -UPS_category ) holds a is Object of C iff P[a] from YELLOW20:sch 2( A2);

      end;

      correctness

      proof

        let B1,B2 be strict full non empty subcategory of (W -UPS_category ) such that

         A3: for a be Object of (W -UPS_category ) holds a is Object of B1 iff P[a] and

         A4: for a be Object of (W -UPS_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

    definition

      let W be with_non-empty_element set;

      defpred P[ Object of (W -CONT_category )] means ( latt $1) is algebraic;

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

      :: YELLOW21:def12

      func W -ALG_category -> strict full non empty subcategory of (W -CONT_category ) means

      : Def12: for a be Object of (W -CONT_category ) holds a is Object of it iff ( latt a) is algebraic;

      existence

      proof

        reconsider b as Object of (W -UPS_category ) by A1, Def10;

        b = ( latt b);

        then

        reconsider b as Object of (W -CONT_category ) by Def11;

        b = ( latt b);

        then

         A2: ex b be Object of (W -CONT_category ) st P[b];

        thus ex C be strict full non empty subcategory of (W -CONT_category ) st for a be Object of (W -CONT_category ) holds a is Object of C iff P[a] from YELLOW20:sch 2( A2);

      end;

      correctness

      proof

        let B1,B2 be strict full non empty subcategory of (W -CONT_category ) such that

         A3: for a be Object of (W -CONT_category ) holds a is Object of B1 iff P[a] and

         A4: for a be Object of (W -CONT_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 :: YELLOW21:16

    

     Th16: 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 -CONT_category ) iff L is strict complete continuous

    proof

      let W be with_non-empty_element set, L be LATTICE such that

       A1: the carrier of L in W;

      hereby

        assume L is Object of (W -CONT_category );

        then

        reconsider a = L as Object of (W -CONT_category );

        L = ( latt a) & a is Object of (W -UPS_category ) by ALTCAT_2: 29;

        hence L is strict complete continuous by A1, Def11, Th14;

      end;

      assume

       A2: L is strict complete continuous;

      then

      reconsider a = L as Object of (W -UPS_category ) by A1, Th14;

      ( latt a) = L;

      hence thesis by A2, Def11;

    end;

    theorem :: YELLOW21:17

    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 -ALG_category ) iff L is strict complete algebraic

    proof

      let W be with_non-empty_element set, L be LATTICE such that

       A1: the carrier of L in W;

      hereby

        assume L is Object of (W -ALG_category );

        then

        reconsider a = L as Object of (W -ALG_category );

        L = ( latt a) & a is Object of (W -CONT_category ) by ALTCAT_2: 29;

        hence L is strict complete algebraic by A1, Def12, Th16;

      end;

      assume

       A2: L is strict complete algebraic;

      then

      reconsider a = L as Object of (W -CONT_category ) by A1, Th16;

      ( latt a) = L;

      hence thesis by A2, Def12;

    end;

    theorem :: YELLOW21:18

    

     Th18: for W be with_non-empty_element set holds for a,b be Object of (W -CONT_category ) holds for f be set holds f in <^a, b^> iff f is 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 -CONT_category ), f be set;

      reconsider a1 = a, b1 = b as Object of (W -UPS_category ) by ALTCAT_2: 29;

       <^a, b^> = <^a1, b1^> by ALTCAT_2: 28;

      hence thesis by Th15;

    end;

    theorem :: YELLOW21:19

    

     Th19: for W be with_non-empty_element set holds for a,b be Object of (W -ALG_category ) holds for f be set holds f in <^a, b^> iff f is 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 -ALG_category ), f be set;

      reconsider a1 = a, b1 = b as Object of (W -CONT_category ) by ALTCAT_2: 29;

       <^a, b^> = <^a1, b1^> by ALTCAT_2: 28;

      hence thesis by Th18;

    end;

    registration

      let W be with_non-empty_element set;

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

      cluster <^a, b^> -> non empty;

      coherence

      proof

        set f = the directed-sups-preserving Function of ( latt a), ( latt b);

        f in <^a, b^> by Th18;

        hence thesis;

      end;

    end

    registration

      let W be with_non-empty_element set;

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

      cluster <^a, b^> -> non empty;

      coherence

      proof

        set f = the directed-sups-preserving Function of ( latt a), ( latt b);

        f in <^a, b^> by Th19;

        hence thesis;

      end;

    end