waybel10.miz



    begin

    scheme :: WAYBEL10:sch1

    SubrelstrEx { L() -> non empty RelStr , P[ object], a() -> set } :

ex S be non empty full strict SubRelStr of L() st for x be Element of L() holds x is Element of S iff P[x]

      provided

       A1: P[a()]

       and

       A2: a() in the carrier of L();

      consider A be set such that

       A3: for x be object holds x in A iff x in the carrier of L() & P[x] from XBOOLE_0:sch 1;

      A c= the carrier of L() by A3;

      then

      reconsider A as non empty Subset of L() by A1, A2, A3;

      set S = ( subrelstr A);

      take S;

      let x be Element of L();

      

       A4: the carrier of S = A by YELLOW_0:def 15;

      hence x is Element of S implies P[x] by A3;

      assume P[x];

      hence thesis by A3, A4;

    end;

    scheme :: WAYBEL10:sch2

    RelstrEq { L1,L2() -> non empty RelStr , P[ object], Q[ set, set] } :

the RelStr of L1() = the RelStr of L2()

      provided

       A1: for x be object holds x is Element of L1() iff P[x]

       and

       A2: for x be object holds x is Element of L2() iff P[x]

       and

       A3: for a,b be Element of L1() holds a <= b iff Q[a, b]

       and

       A4: for a,b be Element of L2() holds a <= b iff Q[a, b];

      set S1 = L1(), S2 = L2();

      

       A5: the carrier of L1() = the carrier of L2()

      proof

        hereby

          let x be object;

          assume x in the carrier of S1;

          then

          reconsider y = x as Element of S1;

          P[y] by A1;

          then x is Element of S2 by A2;

          hence x in the carrier of S2;

        end;

        let x be object;

        assume x in the carrier of S2;

        then

        reconsider y = x as Element of S2;

        P[y] by A2;

        then x is Element of S1 by A1;

        hence thesis;

      end;

      the InternalRel of L1() = the InternalRel of L2()

      proof

        let x,y be object;

        hereby

          assume

           A6: [x, y] in the InternalRel of S1;

          then

          reconsider x1 = x, y1 = y as Element of S1 by ZFMISC_1: 87;

          reconsider x2 = x1, y2 = y1 as Element of S2 by A5;

          x1 <= y1 by A6;

          then Q[x1, y1] by A3;

          then x2 <= y2 by A4;

          hence [x, y] in the InternalRel of S2;

        end;

        assume

         A7: [x, y] in the InternalRel of S2;

        then

        reconsider x2 = x, y2 = y as Element of S2 by ZFMISC_1: 87;

        reconsider x1 = x2, y1 = y2 as Element of S1 by A5;

        x2 <= y2 by A7;

        then Q[x2, y2] by A4;

        then x1 <= y1 by A3;

        hence thesis;

      end;

      hence thesis by A5;

    end;

    scheme :: WAYBEL10:sch3

    SubrelstrEq1 { L() -> non empty RelStr , S1,S2() -> non empty full SubRelStr of L() , P[ object] } :

the RelStr of S1() = the RelStr of S2()

      provided

       A1: for x be object holds x is Element of S1() iff P[x]

       and

       A2: for x be object holds x is Element of S2() iff P[x];

      

       A3: for x be object holds x is Element of S2() iff P[x] by A2;

      defpred Q[ set, set] means [$1, $2] in the InternalRel of L();

       A4:

      now

        let a,b be Element of S1();

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

        x <= y iff [x, y] in the InternalRel of L();

        hence a <= b iff Q[a, b] by YELLOW_0: 59, YELLOW_0: 60;

      end;

       A5:

      now

        let a,b be Element of S2();

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

        x <= y iff [x, y] in the InternalRel of L();

        hence a <= b iff Q[a, b] by YELLOW_0: 59, YELLOW_0: 60;

      end;

      

       A6: for x be object holds x is Element of S1() iff P[x] by A1;

      thus thesis from RelstrEq( A6, A3, A4, A5);

    end;

    scheme :: WAYBEL10:sch4

    SubrelstrEq2 { L() -> non empty RelStr , S1,S2() -> non empty full SubRelStr of L() , P[ object] } :

the RelStr of S1() = the RelStr of S2()

      provided

       A1: for x be Element of L() holds x is Element of S1() iff P[x]

       and

       A2: for x be Element of L() holds x is Element of S2() iff P[x];

      defpred p[ object] means P[$1] & $1 is Element of L();

       A3:

      now

        let x be object;

        x is Element of S2() implies x is Element of L() by YELLOW_0: 58;

        hence x is Element of S2() iff p[x] by A2;

      end;

       A4:

      now

        let x be object;

        x is Element of S1() implies x is Element of L() by YELLOW_0: 58;

        hence x is Element of S1() iff p[x] by A1;

      end;

      thus thesis from SubrelstrEq1( A4, A3);

    end;

    theorem :: WAYBEL10:1

    

     Th1: for R,Q be Relation holds (R c= Q iff (R ~ ) c= (Q ~ )) & ((R ~ ) c= Q iff R c= (Q ~ ))

    proof

      let R,Q be Relation;

      

       A1: ((Q ~ ) ~ ) = Q;

      ((R ~ ) ~ ) = R;

      hence thesis by A1, SYSREL: 11;

    end;

    theorem :: WAYBEL10:2

    

     Th2: for L,S be RelStr holds (S is SubRelStr of L iff (S opp ) is SubRelStr of (L opp )) & ((S opp ) is SubRelStr of L iff S is SubRelStr of (L opp ))

    proof

      let L,S be RelStr;

      thus S is SubRelStr of L implies (S opp ) is SubRelStr of (L opp )

      proof

        assume that

         A1: the carrier of S c= the carrier of L and

         A2: the InternalRel of S c= the InternalRel of L;

        thus the carrier of (S opp ) c= the carrier of (L opp ) & the InternalRel of (S opp ) c= the InternalRel of (L opp ) by A1, A2, Th1;

      end;

      thus (S opp ) is SubRelStr of (L opp ) implies S is SubRelStr of L

      proof

        assume that

         A3: the carrier of (S opp ) c= the carrier of (L opp ) and

         A4: the InternalRel of (S opp ) c= the InternalRel of (L opp );

        thus the carrier of S c= the carrier of L & the InternalRel of S c= the InternalRel of L by A3, A4, Th1;

      end;

      thus (S opp ) is SubRelStr of L implies S is SubRelStr of (L opp )

      proof

        assume that

         A5: the carrier of (S opp ) c= the carrier of L and

         A6: the InternalRel of (S opp ) c= the InternalRel of L;

        thus the carrier of S c= the carrier of (L opp ) & the InternalRel of S c= the InternalRel of (L opp ) by A5, A6, Th1;

      end;

      assume that

       A7: the carrier of S c= the carrier of (L opp ) and

       A8: the InternalRel of S c= the InternalRel of (L opp );

      thus the carrier of (S opp ) c= the carrier of L & the InternalRel of (S opp ) c= the InternalRel of L by A7, A8, Th1;

    end;

    theorem :: WAYBEL10:3

    

     Th3: for L,S be RelStr holds (S is full SubRelStr of L iff (S opp ) is full SubRelStr of (L opp )) & ((S opp ) is full SubRelStr of L iff S is full SubRelStr of (L opp ))

    proof

      let L,S be RelStr;

      

       A1: ((the InternalRel of L |_2 the carrier of S) ~ ) = ((the InternalRel of L ~ ) |_2 the carrier of S) by ORDERS_1: 83;

      hereby

        assume

         A2: S is full SubRelStr of L;

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

        hence (S opp ) is full SubRelStr of (L opp ) by A1, A2, Th2, YELLOW_0:def 14;

      end;

      

       A3: (((the InternalRel of L ~ ) |_2 the carrier of S) ~ ) = (((the InternalRel of L ~ ) ~ ) |_2 the carrier of S) by ORDERS_1: 83;

      hereby

        assume

         A4: (S opp ) is full SubRelStr of (L opp );

        then the InternalRel of (S opp ) = (the InternalRel of (L opp ) |_2 the carrier of S) by YELLOW_0:def 14;

        hence S is full SubRelStr of L by A3, A4, Th2, YELLOW_0:def 14;

      end;

      hereby

        assume

         A5: (S opp ) is full SubRelStr of L;

        then the InternalRel of (S opp ) = (the InternalRel of L |_2 the carrier of S) by YELLOW_0:def 14;

        hence S is full SubRelStr of (L opp ) by A1, A5, Th2, YELLOW_0:def 14;

      end;

      assume

       A6: S is full SubRelStr of (L opp );

      then the InternalRel of S = (the InternalRel of (L opp ) |_2 the carrier of S) by YELLOW_0:def 14;

      hence thesis by A1, A6, Th2, YELLOW_0:def 14;

    end;

    definition

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

      :: original: opp

      redefine

      func S opp -> strict full SubRelStr of (L opp ) ;

      coherence by Th3;

    end

    registration

      let X be set, L be non empty RelStr;

      cluster (X --> L) -> non-Empty;

      coherence

      proof

        let R be 1-sorted;

        assume R in ( rng (X --> L));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let S be RelStr, T be non empty reflexive RelStr;

      cluster monotone for Function of S, T;

      existence

      proof

        set c = the Element of T;

        take f = (S --> c);

        let x,y be Element of S;

        assume [x, y] in the InternalRel of S;

        then

         A1: x in the carrier of S by ZFMISC_1: 87;

        let a,b be Element of T;

        assume that

         A2: a = (f . x) and

         A3: b = (f . y);

        a = c by A1, A2, FUNCOP_1: 7;

        hence a <= b by A1, A3, FUNCOP_1: 7;

      end;

    end

    registration

      let L be non empty RelStr;

      cluster projection -> monotone idempotent for Function of L, L;

      coherence by WAYBEL_1:def 13;

    end

    registration

      let S,T be non empty reflexive RelStr;

      let f be monotone Function of S, T;

      cluster ( corestr f) -> monotone;

      coherence

      proof

        let x,y be Element of S;

        

         A1: (f . y) = (( corestr f) . y) by WAYBEL_1: 30;

        assume x <= y;

        then

         A2: (f . x) <= (f . y) by WAYBEL_1:def 2;

        (f . x) = (( corestr f) . x) by WAYBEL_1: 30;

        hence thesis by A2, A1, YELLOW_0: 60;

      end;

    end

    registration

      let L be non empty reflexive RelStr;

      cluster ( id L) -> sups-preserving infs-preserving;

      coherence

      proof

        thus ( id L) is sups-preserving

        proof

          let X be Subset of L;

          assume ex_sup_of (X,L);

          hence thesis by FUNCT_1: 92;

        end;

        let X be Subset of L;

        assume ex_inf_of (X,L);

        hence thesis by FUNCT_1: 92;

      end;

    end

    theorem :: WAYBEL10:4

    for L be RelStr, S be Subset of L holds ( id S) is Function of ( subrelstr S), L & for f be Function of ( subrelstr S), L st f = ( id S) holds f is monotone

    proof

      let L be RelStr, S be Subset of L;

      

       A1: the carrier of ( subrelstr S) = S by YELLOW_0:def 15;

      

       A2: ( rng ( id S)) = S by RELAT_1: 45;

      ( dom ( id S)) = S by RELAT_1: 45;

      hence ( id S) is Function of ( subrelstr S), L by A1, A2, FUNCT_2: 2;

      let f be Function of ( subrelstr S), L;

      assume

       A3: f = ( id S);

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

      assume

       A4: [x, y] in the InternalRel of ( subrelstr S);

      let a,b be Element of L;

      assume that

       A5: a = (f . x) and

       A6: b = (f . y);

      x in S by A1, A4, ZFMISC_1: 87;

      then

       A7: a = x by A3, A5, FUNCT_1: 17;

      y in S by A1, A4, ZFMISC_1: 87;

      then

       A8: b = y by A3, A6, FUNCT_1: 17;

      the InternalRel of ( subrelstr S) c= the InternalRel of L by YELLOW_0:def 13;

      hence [a, b] in the InternalRel of L by A4, A7, A8;

    end;

    registration

      let L be non empty reflexive RelStr;

      cluster sups-preserving infs-preserving closure kernel one-to-one for Function of L, L;

      existence

      proof

        take ( id L);

        thus thesis;

      end;

    end

    theorem :: WAYBEL10:5

    

     Th5: for L be non empty reflexive RelStr, c be closure Function of L, L holds for x be Element of L holds (c . x) >= x

    proof

      let L be non empty reflexive RelStr, c be closure Function of L, L;

      let x be Element of L;

      c >= ( id L) by WAYBEL_1:def 14;

      then (c . x) >= (( id L) . x) by YELLOW_2: 9;

      hence thesis;

    end;

    theorem :: WAYBEL10:6

    

     Th6: for S,T be RelStr, R be SubRelStr of S holds for f be Function of the carrier of S, the carrier of T holds (f | R) = (f | the carrier of R) & for x be set st x in the carrier of R holds ((f | R) . x) = (f . x)

    proof

      let S,T be RelStr, R be SubRelStr of S;

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

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

      hence (f | R) = (f | the carrier of R) by TMAP_1:def 3;

      hence thesis by FUNCT_1: 49;

    end;

    theorem :: WAYBEL10:7

    

     Th7: for S,T be RelStr, f be Function of S, T st f is one-to-one holds for R be SubRelStr of S holds (f | R) is one-to-one

    proof

      let S,T be RelStr, f be Function of S, T such that

       A1: f is one-to-one;

      let R be SubRelStr of S;

      (f | R) = (f | the carrier of R) by Th6;

      hence thesis by A1, FUNCT_1: 52;

    end;

    registration

      let S,T be non empty reflexive RelStr;

      let f be monotone Function of S, T;

      let R be SubRelStr of S;

      cluster (f | R) -> monotone;

      coherence

      proof

        let x,y be Element of R;

        

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

        assume

         A2: x <= y;

        then

         A3: [x, y] in the InternalRel of R;

        then

         A4: x in the carrier of R by ZFMISC_1: 87;

        y in the carrier of R by A3, ZFMISC_1: 87;

        then

        reconsider a = x, b = y as Element of S by A1;

        

         A5: a <= b by A2, YELLOW_0: 59;

        

         A6: (f . b) = ((f | R) . y) by A4, Th6;

        (f . a) = ((f | R) . x) by A4, Th6;

        hence thesis by A5, A6, WAYBEL_1:def 2;

      end;

    end

    theorem :: WAYBEL10:8

    

     Th8: for S,T be non empty RelStr, R be non empty SubRelStr of S holds for f be Function of S, T, g be Function of T, S st f is one-to-one & g = (f " ) holds (g | ( Image (f | R))) is Function of ( Image (f | R)), R & (g | ( Image (f | R))) = ((f | R) " )

    proof

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

      let f be Function of S, T, g be Function of T, S;

      assume that

       A1: f is one-to-one and

       A2: g = (f " );

      set h = (g | ( Image (f | R)));

      

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

      

       A4: ( dom h) = the carrier of ( Image (f | R)) by FUNCT_2:def 1;

      

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

      ( rng h) c= the carrier of R

      proof

        let y be object;

        assume y in ( rng h);

        then

        consider x be object such that

         A6: x in ( dom h) and

         A7: y = (h . x) by FUNCT_1:def 3;

        reconsider x as Element of ( Image (f | R)) by A6;

        consider a be Element of R such that

         A8: ((f | R) . a) = x by YELLOW_2: 10;

        

         A9: (f . a) = x by A8, Th6;

        

         A10: a in the carrier of R;

        y = (g . x) by A7, Th6;

        hence thesis by A1, A2, A5, A3, A10, A9, FUNCT_1: 32;

      end;

      hence h is Function of ( Image (f | R)), R by A4, RELSET_1: 4;

      

       A11: ( rng (f | R)) = the carrier of ( Image (f | R)) by YELLOW_0:def 15;

      

       A12: (f | R) is one-to-one by A1, Th7;

       A13:

      now

        let x be object;

        

         A14: ( dom (f | R)) = the carrier of R by FUNCT_2:def 1;

        assume

         A15: x in the carrier of ( Image (f | R));

        then

        consider y be object such that

         A16: y in ( dom (f | R)) and

         A17: x = ((f | R) . y) by A11, FUNCT_1:def 3;

        

         A18: y = (((f | R) " ) . x) by A12, A16, A17, FUNCT_1: 32;

        x = (f . y) by A16, A17, Th6;

        then y = (g . x) by A1, A2, A5, A3, A16, A14, FUNCT_1: 32;

        hence (h . x) = (((f | R) " ) . x) by A15, A18, Th6;

      end;

      ( dom ((f | R) " )) = ( rng (f | R)) by A12, FUNCT_1: 33;

      hence thesis by A4, A11, A13, FUNCT_1: 2;

    end;

    begin

    registration

      let S be RelStr, T be non empty reflexive RelStr;

      cluster ( MonMaps (S,T)) -> non empty;

      coherence

      proof

        set f = the monotone Function of S, T;

        f in ( Funcs (the carrier of S,the carrier of T)) by FUNCT_2: 8;

        hence thesis by YELLOW_1:def 6;

      end;

    end

    theorem :: WAYBEL10:9

    

     Th9: for S be RelStr, T be non empty reflexive RelStr, x be set holds x is Element of ( MonMaps (S,T)) iff x is monotone Function of S, T

    proof

      let S be RelStr, T be non empty reflexive RelStr;

      let x be set;

      hereby

        assume x is Element of ( MonMaps (S,T));

        then

        reconsider f = x as Element of ( MonMaps (S,T));

        f is Element of (T |^ the carrier of S) by YELLOW_0: 58;

        then f in the carrier of (T |^ the carrier of S);

        then f in ( Funcs (the carrier of S,the carrier of T)) by YELLOW_1: 28;

        then

        reconsider f as Function of S, T by FUNCT_2: 66;

        f in the carrier of ( MonMaps (S,T));

        hence x is monotone Function of S, T by YELLOW_1:def 6;

      end;

      assume x is monotone Function of S, T;

      then

      reconsider f = x as monotone Function of S, T;

      f in ( Funcs (the carrier of S,the carrier of T)) by FUNCT_2: 8;

      hence thesis by YELLOW_1:def 6;

    end;

    definition

      let L be non empty reflexive RelStr;

      :: WAYBEL10:def1

      func ClOpers L -> non empty full strict SubRelStr of ( MonMaps (L,L)) means

      : Def1: for f be Function of L, L holds f is Element of it iff f is closure;

      existence

      proof

        defpred P[ set] means $1 is closure Function of L, L;

        set h = the closure Function of L, L;

        h in ( Funcs (the carrier of L,the carrier of L)) by FUNCT_2: 9;

        then

         A1: h in the carrier of ( MonMaps (L,L)) by YELLOW_1:def 6;

        

         A2: P[h];

        consider S be non empty full strict SubRelStr of ( MonMaps (L,L)) such that

         A3: for f be Element of ( MonMaps (L,L)) holds f is Element of S iff P[f] from SubrelstrEx( A2, A1);

        take S;

        let f be Function of L, L;

        hereby

          assume

           A4: f is Element of S;

          then f is Element of ( MonMaps (L,L)) by YELLOW_0: 58;

          hence f is closure by A3, A4;

        end;

        assume

         A5: f is closure;

        f in ( Funcs (the carrier of L,the carrier of L)) by FUNCT_2: 9;

        then f in the carrier of ( MonMaps (L,L)) by A5, YELLOW_1:def 6;

        hence thesis by A3, A5;

      end;

      correctness

      proof

        let S1,S2 be non empty full strict SubRelStr of ( MonMaps (L,L)) such that

         A6: for f be Function of L, L holds f is Element of S1 iff f is closure and

         A7: for f be Function of L, L holds f is Element of S2 iff f is closure;

        the carrier of S1 = the carrier of S2

        proof

          hereby

            let x be object;

            assume x in the carrier of S1;

            then

            reconsider y = x as Element of S1;

            y is Element of ( MonMaps (L,L)) by YELLOW_0: 58;

            then

            reconsider y as Function of L, L by Th9;

            y is closure by A6;

            then y is Element of S2 by A7;

            hence x in the carrier of S2;

          end;

          let x be object;

          assume x in the carrier of S2;

          then

          reconsider y = x as Element of S2;

          y is Element of ( MonMaps (L,L)) by YELLOW_0: 58;

          then

          reconsider y as Function of L, L by Th9;

          y is closure by A7;

          then y is Element of S1 by A6;

          hence thesis;

        end;

        hence thesis by YELLOW_0: 57;

      end;

    end

    theorem :: WAYBEL10:10

    

     Th10: for L be non empty reflexive RelStr, x be set holds x is Element of ( ClOpers L) iff x is closure Function of L, L by YELLOW_0: 58, Def1, Th9;

    theorem :: WAYBEL10:11

    

     Th11: for X be set, L be non empty RelStr holds for f,g be Function of X, the carrier of L holds for x,y be Element of (L |^ X) st x = f & y = g holds x <= y iff f <= g

    proof

      let X be set, L be non empty RelStr;

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

      let x,y be Element of (L |^ X) such that

       A1: x = f and

       A2: y = g;

      set J = (X --> L);

      

       A3: (L |^ X) = ( product J) by YELLOW_1:def 5;

      

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

      then

       A5: x <= y iff ex f,g be Function st f = x & g = y & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A3, YELLOW_1:def 4;

      hereby

        assume

         A6: x <= y;

        thus f <= g

        proof

          let i be set;

          assume

           A7: i in X;

          then

           A8: (J . i) = L by FUNCOP_1: 7;

          ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A1, A2, A5, A6, A7;

          hence thesis by A8;

        end;

      end;

      assume

       A9: for j be set st j in X holds ex a,b be Element of L st a = (f . j) & b = (g . j) & a <= b;

      now

        reconsider f9 = f, g9 = g as Function;

        take f9, g9;

        thus f9 = x & g9 = y by A1, A2;

        let i be object;

        assume

         A10: i in X;

        then

         A11: (J . i) = L by FUNCOP_1: 7;

        ex a,b be Element of L st a = (f . i) & b = (g . i) & a <= b by A9, A10;

        hence ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f9 . i) & yi = (g9 . i) & xi <= yi by A11;

      end;

      hence thesis by A4, A3, YELLOW_1:def 4;

    end;

    theorem :: WAYBEL10:12

    

     Th12: for L be complete LATTICE holds for c1,c2 be Function of L, L holds for x,y be Element of ( ClOpers L) st x = c1 & y = c2 holds x <= y iff c1 <= c2

    proof

      let L be complete LATTICE;

      let c1,c2 be Function of L, L, x,y be Element of ( ClOpers L) such that

       A1: x = c1 and

       A2: y = c2;

      reconsider x9 = x, y9 = y as Element of ( MonMaps (L,L)) by YELLOW_0: 58;

      reconsider x99 = x9, y99 = y9 as Element of (L |^ the carrier of L) by YELLOW_0: 58;

      x99 <= y99 iff x9 <= y9 by YELLOW_0: 59, YELLOW_0: 60;

      hence thesis by A1, A2, Th11, YELLOW_0: 59, YELLOW_0: 60;

    end;

    theorem :: WAYBEL10:13

    

     Th13: for L be reflexive RelStr, S1,S2 be full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds S1 is SubRelStr of S2

    proof

      let L be reflexive RelStr, S1,S2 be full SubRelStr of L;

      assume

       A1: the carrier of S1 c= the carrier of S2;

      hence the carrier of S1 c= the carrier of S2;

      let x,y be object;

      assume

       A2: [x, y] in the InternalRel of S1;

      then

       A3: x in the carrier of S1 by ZFMISC_1: 87;

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

      the carrier of S1 c= the carrier of L by YELLOW_0:def 13;

      then

      reconsider a = x, b = y as Element of L by A3;

      reconsider x9 = x, y9 = y as Element of S2 by A1, A3;

      x <= y by A2;

      then a <= b by YELLOW_0: 59;

      then x9 <= y9 by A1, A3, YELLOW_0: 60;

      hence thesis;

    end;

    theorem :: WAYBEL10:14

    

     Th14: for L be complete LATTICE holds for c1,c2 be closure Function of L, L holds c1 <= c2 iff ( Image c2) is SubRelStr of ( Image c1)

    proof

      let L be complete LATTICE;

      let c1,c2 be closure Function of L, L;

      hereby

        assume

         A1: c1 <= c2;

        the carrier of ( Image c2) c= the carrier of ( Image c1)

        proof

          let x be object;

          assume x in the carrier of ( Image c2);

          then

          consider y be Element of L such that

           A2: (c2 . y) = x by YELLOW_2: 10;

          

           A3: (c2 . (c2 . y)) = (c2 . y) by YELLOW_2: 18;

          

           A4: (c1 . (c2 . y)) <= (c2 . (c2 . y)) by A1, YELLOW_2: 9;

          (c2 . y) <= (c1 . (c2 . y)) by Th5;

          then (c1 . (c2 . y)) = x by A2, A4, A3, ORDERS_2: 2;

          then x in ( rng c1) by FUNCT_2: 4;

          hence thesis by YELLOW_0:def 15;

        end;

        hence ( Image c2) is SubRelStr of ( Image c1) by Th13;

      end;

      assume that

       A5: the carrier of ( Image c2) c= the carrier of ( Image c1) and the InternalRel of ( Image c2) c= the InternalRel of ( Image c1);

      now

        let x be Element of L;

        (c2 . x) in ( rng c2) by FUNCT_2: 4;

        then (c2 . x) in the carrier of ( Image c2) by YELLOW_0:def 15;

        then ex a be Element of L st (c1 . a) = (c2 . x) by A5, YELLOW_2: 10;

        then

         A6: (c1 . (c2 . x)) = (c2 . x) by YELLOW_2: 18;

        x <= (c2 . x) by Th5;

        hence (c1 . x) <= (c2 . x) by A6, WAYBEL_1:def 2;

      end;

      hence thesis by YELLOW_2: 9;

    end;

    begin

    definition

      let L be RelStr;

      :: WAYBEL10:def2

      func Sub L -> strict non empty RelStr means

      : Def2: (for x be object holds x is Element of it iff x is strict SubRelStr of L) & for a,b be Element of it holds a <= b iff ex R be RelStr st b = R & a is SubRelStr of R;

      existence

      proof

        set X = { RelStr (# A, B #) where A be Subset of L, B be Relation of A, A : B c= the InternalRel of L };

        

         A1: the InternalRel of ( subrelstr ( {} L)) c= the InternalRel of L by YELLOW_0:def 13;

        the carrier of ( subrelstr ( {} L)) = ( {} L) by YELLOW_0:def 15;

        then ( subrelstr ( {} L)) in X by A1;

        then

        reconsider X as non empty set;

        defpred P[ set, set] means ex R be RelStr st $2 = R & $1 is SubRelStr of R;

        consider S be strict non empty RelStr such that

         A2: the carrier of S = X and

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

        take S;

        hereby

          let x be object;

          hereby

            assume x is Element of S;

            then x in X by A2;

            then ex A be Subset of L, B be Relation of A, A st x = RelStr (# A, B #) & B c= the InternalRel of L;

            hence x is strict SubRelStr of L by YELLOW_0:def 13;

          end;

          assume x is strict SubRelStr of L;

          then

          reconsider R = x as strict SubRelStr of L;

          

           A4: the InternalRel of R c= the InternalRel of L by YELLOW_0:def 13;

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

          then R in X by A4;

          hence x is Element of S by A2;

        end;

        thus thesis by A3;

      end;

      correctness

      proof

        defpred Q[ set, set] means ex R be RelStr st $2 = R & $1 is SubRelStr of R;

        defpred P[ object] means $1 is strict SubRelStr of L;

        let S1,S2 be non empty strict RelStr such that

         A5: for x be object holds x is Element of S1 iff P[x] and

         A6: for a,b be Element of S1 holds a <= b iff Q[a, b] and

         A7: for x be object holds x is Element of S2 iff P[x] and

         A8: for a,b be Element of S2 holds a <= b iff Q[a, b];

         the RelStr of S1 = the RelStr of S2 from RelstrEq( A5, A7, A6, A8);

        hence thesis;

      end;

    end

    theorem :: WAYBEL10:15

    

     Th15: for L,R be RelStr holds for x,y be Element of ( Sub L) st y = R holds x <= y iff x is SubRelStr of R

    proof

      let L,R be RelStr;

      let x,y be Element of ( Sub L);

      x <= y iff ex R be RelStr st y = R & x is SubRelStr of R by Def2;

      hence thesis;

    end;

    registration

      let L be RelStr;

      cluster ( Sub L) -> reflexive antisymmetric transitive;

      coherence

      proof

        set R = ( Sub L);

        thus R is reflexive

        proof

          let x be Element of R;

          reconsider A = x as strict SubRelStr of L by Def2;

          A is SubRelStr of A by YELLOW_0:def 13;

          hence thesis by Th15;

        end;

        thus R is antisymmetric

        proof

          let x,y be Element of R;

          reconsider A = x, B = y as strict SubRelStr of L by Def2;

          assume that

           A1: x <= y and

           A2: y <= x;

          

           A3: B is SubRelStr of A by A2, Th15;

          then

           A4: the carrier of B c= the carrier of A by YELLOW_0:def 13;

          

           A5: A is SubRelStr of B by A1, Th15;

          then the carrier of A c= the carrier of B by YELLOW_0:def 13;

          then

           A6: the carrier of A = the carrier of B by A4;

          

           A7: the InternalRel of B c= the InternalRel of A by A3, YELLOW_0:def 13;

          the InternalRel of A c= the InternalRel of B by A5, YELLOW_0:def 13;

          hence thesis by A7, A6, XBOOLE_0:def 10;

        end;

        thus R is transitive

        proof

          let x,y,z be Element of R;

          reconsider A = x, B = y, C = z as strict SubRelStr of L by Def2;

          assume that

           A8: x <= y and

           A9: y <= z;

          

           A10: B is SubRelStr of C by A9, Th15;

          then

           A11: the carrier of B c= the carrier of C by YELLOW_0:def 13;

          

           A12: the InternalRel of B c= the InternalRel of C by A10, YELLOW_0:def 13;

          

           A13: A is SubRelStr of B by A8, Th15;

          then the InternalRel of A c= the InternalRel of B by YELLOW_0:def 13;

          then

           A14: the InternalRel of A c= the InternalRel of C by A12;

          the carrier of A c= the carrier of B by A13, YELLOW_0:def 13;

          then the carrier of A c= the carrier of C by A11;

          then A is SubRelStr of C by A14, YELLOW_0:def 13;

          hence thesis by Th15;

        end;

      end;

    end

    registration

      let L be RelStr;

      cluster ( Sub L) -> complete;

      coherence

      proof

        now

          let X be Subset of ( Sub L);

          now

            defpred Q[ object] means ex R be RelStr st R in X & $1 in the InternalRel of R;

            defpred P[ object] means ex R be RelStr st R in X & $1 in the carrier of R;

            consider Y be set such that

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

            consider S be set such that

             A2: for x be object holds x in S iff x in the InternalRel of L & Q[x] from XBOOLE_0:sch 1;

            

             A3: S c= [:Y, Y:]

            proof

              let x be object;

              assume x in S;

              then

              consider R be RelStr such that

               A4: R in X and

               A5: x in the InternalRel of R by A2;

              the carrier of R c= Y

              proof

                let x be object;

                R is SubRelStr of L by A4, Def2;

                then

                 A6: the carrier of R c= the carrier of L by YELLOW_0:def 13;

                assume x in the carrier of R;

                hence thesis by A1, A4, A6;

              end;

              then

               A7: [:the carrier of R, the carrier of R:] c= [:Y, Y:] by ZFMISC_1: 96;

              x in [:the carrier of R, the carrier of R:] by A5;

              hence thesis by A7;

            end;

            

             A8: S c= the InternalRel of L by A2;

            reconsider S as Relation of Y by A3;

            Y c= the carrier of L by A1;

            then

            reconsider A = RelStr (# Y, S #) as SubRelStr of L by A8, YELLOW_0:def 13;

            reconsider a = A as Element of ( Sub L) by Def2;

            take a;

            thus X is_<=_than a

            proof

              let b be Element of ( Sub L);

              reconsider R = b as strict SubRelStr of L by Def2;

              assume

               A9: b in X;

              

               A10: the InternalRel of R c= S

              proof

                let x,y be object;

                

                 A11: the InternalRel of R c= the InternalRel of L by YELLOW_0:def 13;

                assume [x, y] in the InternalRel of R;

                hence thesis by A2, A9, A11;

              end;

              the carrier of R c= Y

              proof

                let x be object;

                

                 A12: the carrier of R c= the carrier of L by YELLOW_0:def 13;

                assume x in the carrier of R;

                hence thesis by A1, A9, A12;

              end;

              then R is SubRelStr of A by A10, YELLOW_0:def 13;

              hence b <= a by Th15;

            end;

            let b be Element of ( Sub L);

            reconsider B = b as strict SubRelStr of L by Def2;

            assume

             A13: X is_<=_than b;

            

             A14: S c= the InternalRel of B

            proof

              let x,y be object;

              assume [x, y] in S;

              then

              consider R be RelStr such that

               A15: R in X and

               A16: [x, y] in the InternalRel of R by A2;

              reconsider c = R as Element of ( Sub L) by A15;

              c <= b by A13, A15;

              then R is SubRelStr of B by Th15;

              then the InternalRel of R c= the InternalRel of B by YELLOW_0:def 13;

              hence thesis by A16;

            end;

            Y c= the carrier of B

            proof

              let x be object;

              assume x in Y;

              then

              consider R be RelStr such that

               A17: R in X and

               A18: x in the carrier of R by A1;

              reconsider c = R as Element of ( Sub L) by A17;

              c <= b by A13, A17;

              then R is SubRelStr of B by Th15;

              then the carrier of R c= the carrier of B by YELLOW_0:def 13;

              hence thesis by A18;

            end;

            then a is SubRelStr of B by A14, YELLOW_0:def 13;

            hence a <= b by Th15;

          end;

          hence ex_sup_of (X,( Sub L)) by YELLOW_0: 15;

        end;

        hence thesis by YELLOW_0: 53;

      end;

    end

    registration

      let L be complete LATTICE;

      cluster infs-inheriting -> non empty for SubRelStr of L;

      coherence

      proof

        let S be SubRelStr of L such that

         A1: S is infs-inheriting;

         ex_inf_of (( {} S),L) by YELLOW_0: 17;

        hence thesis by A1;

      end;

      cluster sups-inheriting -> non empty for SubRelStr of L;

      coherence

      proof

        let S be SubRelStr of L such that

         A2: S is sups-inheriting;

         ex_sup_of (( {} S),L) by YELLOW_0: 17;

        hence thesis by A2;

      end;

    end

    definition

      let L be RelStr;

      mode System of L is full SubRelStr of L;

    end

    notation

      let L be non empty RelStr;

      let S be System of L;

      synonym S is closure for S is infs-inheriting;

    end

    registration

      let L be non empty RelStr;

      cluster ( subrelstr ( [#] L)) -> infs-inheriting sups-inheriting;

      coherence

      proof

        set SL = ( subrelstr ( [#] L));

        

         A1: the carrier of SL = the carrier of L by YELLOW_0:def 15;

        thus SL is infs-inheriting by A1;

        let X be Subset of SL;

        thus thesis by A1;

      end;

    end

    definition

      let L be non empty RelStr;

      :: WAYBEL10:def3

      func ClosureSystems L -> full strict non empty SubRelStr of ( Sub L) means

      : Def3: for R be strict SubRelStr of L holds R is Element of it iff R is infs-inheriting full;

      existence

      proof

        defpred P[ set] means $1 is infs-inheriting full SubRelStr of L;

        set SL = ( subrelstr ( [#] L));

        SL is Element of ( Sub L) by Def2;

        then

         A1: SL in the carrier of ( Sub L);

        

         A2: P[SL];

        consider S be non empty full strict SubRelStr of ( Sub L) such that

         A3: for x be Element of ( Sub L) holds x is Element of S iff P[x] from SubrelstrEx( A2, A1);

        take S;

        let R be strict SubRelStr of L;

        R is Element of ( Sub L) by Def2;

        hence thesis by A3;

      end;

      correctness

      proof

        defpred P[ object] means $1 is infs-inheriting full strict SubRelStr of L;

        let S1,S2 be full strict non empty SubRelStr of ( Sub L) such that

         A4: for R be strict SubRelStr of L holds R is Element of S1 iff R is infs-inheriting full and

         A5: for R be strict SubRelStr of L holds R is Element of S2 iff R is infs-inheriting full;

         A6:

        now

          let x be object;

          x is Element of S2 implies x is Element of ( Sub L) by YELLOW_0: 58;

          then x is Element of S2 implies x is strict SubRelStr of L by Def2;

          hence x is Element of S2 iff P[x] by A5;

        end;

         A7:

        now

          let x be object;

          x is Element of S1 implies x is Element of ( Sub L) by YELLOW_0: 58;

          then x is Element of S1 implies x is strict SubRelStr of L by Def2;

          hence x is Element of S1 iff P[x] by A4;

        end;

         the RelStr of S1 = the RelStr of S2 from SubrelstrEq1( A7, A6);

        hence thesis;

      end;

    end

    theorem :: WAYBEL10:16

    

     Th16: for L be non empty RelStr, x be object holds x is Element of ( ClosureSystems L) iff x is strict closure System of L

    proof

      let L be non empty RelStr, x be object;

      x is Element of ( ClosureSystems L) implies x is Element of ( Sub L) by YELLOW_0: 58;

      then x is Element of ( ClosureSystems L) implies x is strict SubRelStr of L by Def2;

      hence thesis by Def3;

    end;

    theorem :: WAYBEL10:17

    

     Th17: for L be non empty RelStr, R be RelStr holds for x,y be Element of ( ClosureSystems L) st y = R holds x <= y iff x is SubRelStr of R

    proof

      let L be non empty RelStr, R be RelStr;

      let x,y be Element of ( ClosureSystems L);

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

      x <= y iff a <= b by YELLOW_0: 59, YELLOW_0: 60;

      hence thesis by Th15;

    end;

    begin

    registration

      let L be non empty Poset;

      let h be closure Function of L, L;

      cluster ( Image h) -> infs-inheriting;

      coherence by WAYBEL_1: 53;

    end

    definition

      let L be non empty Poset;

      :: WAYBEL10:def4

      func ClImageMap L -> Function of ( ClOpers L), (( ClosureSystems L) opp ) means

      : Def4: for c be closure Function of L, L holds (it . c) = ( Image c);

      existence

      proof

        defpred P[ set, set] means ex c be closure Function of L, L st c = $1 & $2 = ( Image c);

         A1:

        now

          let x be Element of ( ClOpers L);

          reconsider c = x as closure Function of L, L by Th10;

          reconsider a = ( Image c) as Element of ( ClosureSystems L) by Th16;

          take b = (a ~ );

          thus P[x, b];

        end;

        consider f be Function of ( ClOpers L), (( ClosureSystems L) opp ) such that

         A2: for x be Element of ( ClOpers L) holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        let c be closure Function of L, L;

        c is Element of ( ClOpers L) by Th10;

        then ex c1 be closure Function of L, L st c1 = c & (f . c) = ( Image c1) by A2;

        hence thesis;

      end;

      correctness

      proof

        let f1,f2 be Function of ( ClOpers L), (( ClosureSystems L) opp ) such that

         A3: for c be closure Function of L, L holds (f1 . c) = ( Image c) and

         A4: for c be closure Function of L, L holds (f2 . c) = ( Image c);

        now

          let x be Element of ( ClOpers L);

          reconsider c = x as closure Function of L, L by Th10;

          

          thus (f1 . x) = ( Image c) by A3

          .= (f2 . x) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let L be non empty RelStr;

      let S be SubRelStr of L;

      :: WAYBEL10:def5

      func closure_op S -> Function of L, L means

      : Def5: for x be Element of L holds (it . x) = ( "/\" ((( uparrow x) /\ the carrier of S),L));

      existence

      proof

        deffunc F( Element of L) = ( "/\" ((( uparrow $1) /\ the carrier of S),L));

        thus ex f be Function of L, L st for x be Element of L holds (f . x) = F(x) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let f1,f2 be Function of L, L such that

         A1: for x be Element of L holds (f1 . x) = ( "/\" ((( uparrow x) /\ the carrier of S),L)) and

         A2: for x be Element of L holds (f2 . x) = ( "/\" ((( uparrow x) /\ the carrier of S),L));

        now

          let x be Element of L;

          

          thus (f1 . x) = ( "/\" ((( uparrow x) /\ the carrier of S),L)) by A1

          .= (f2 . x) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    registration

      let L be complete LATTICE;

      let S be closure System of L;

      cluster ( closure_op S) -> closure;

      coherence

      proof

        set c = ( closure_op S);

        reconsider cc = (c * c) as Function of L, L;

         A1:

        now

          let x be Element of L;

          thus (( id L) . x) = x;

          (( uparrow x) /\ the carrier of S) c= ( uparrow x) by XBOOLE_1: 17;

          then

           A2: x is_<=_than (( uparrow x) /\ the carrier of S) by YELLOW_2: 2;

          (c . x) = ( "/\" ((( uparrow x) /\ the carrier of S),L)) by Def5;

          hence (( id L) . x) <= (c . x) by A2, YELLOW_0: 33;

        end;

        now

          let x be Element of L;

          set y = (c . x);

          set X = (( uparrow x) /\ the carrier of S);

          reconsider X as Subset of S by XBOOLE_1: 17;

          

           A3: (c . y) = ( "/\" ((( uparrow y) /\ the carrier of S),L)) by Def5;

          y <= y;

          then

           A4: y in ( uparrow y) by WAYBEL_0: 18;

           ex_inf_of (X,L) by YELLOW_0: 17;

          then

           A5: ( "/\" (X,L)) in the carrier of S by YELLOW_0:def 18;

          y = ( "/\" ((( uparrow x) /\ the carrier of S),L)) by Def5;

          then y in (( uparrow y) /\ the carrier of S) by A5, A4, XBOOLE_0:def 4;

          then

           A6: (c . y) <= y by A3, YELLOW_2: 22;

          

           A7: (c . y) >= (( id L) . y) by A1;

          

          thus (cc . x) = (c . y) by FUNCT_2: 15

          .= (c . x) by A6, A7, ORDERS_2: 2;

        end;

        hence (c * c) = c by FUNCT_2: 63;

        hereby

          let x,y be Element of L;

          

           A8: ex_inf_of ((( uparrow x) /\ the carrier of S),L) by YELLOW_0: 17;

          

           A9: ex_inf_of ((( uparrow y) /\ the carrier of S),L) by YELLOW_0: 17;

          assume x <= y;

          then

           A10: (( uparrow y) /\ the carrier of S) c= (( uparrow x) /\ the carrier of S) by WAYBEL_0: 22, XBOOLE_1: 26;

          

           A11: (c . y) = ( "/\" ((( uparrow y) /\ the carrier of S),L)) by Def5;

          (c . x) = ( "/\" ((( uparrow x) /\ the carrier of S),L)) by Def5;

          hence (c . x) <= (c . y) by A10, A8, A9, A11, YELLOW_0: 35;

        end;

        let x be set;

        assume x in the carrier of L;

        then

        reconsider x as Element of L;

        (( id L) . x) <= (c . x) by A1;

        hence thesis;

      end;

    end

    theorem :: WAYBEL10:18

    

     Th18: for L be complete LATTICE holds for S be closure System of L holds ( Image ( closure_op S)) = the RelStr of S

    proof

      let L be complete LATTICE;

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

      the carrier of ( Image ( closure_op S)) = the carrier of S

      proof

        hereby

          let x be object;

          assume x in the carrier of ( Image ( closure_op S));

          then

          reconsider a = x as Element of ( Image ( closure_op S));

          consider b be Element of L such that

           A1: a = (( closure_op S) . b) by YELLOW_2: 10;

          set X = (( uparrow b) /\ the carrier of S);

          reconsider X as Subset of S by XBOOLE_1: 17;

          

           A2: ex_inf_of (X,L) by YELLOW_0: 17;

          a = ( "/\" (X,L)) by A1, Def5;

          hence x in the carrier of S by A2, YELLOW_0:def 18;

        end;

        set c = ( closure_op S);

        let x be object;

        assume x in the carrier of S;

        then

        reconsider a = x as Element of S;

        reconsider a as Element of L by YELLOW_0: 58;

        set X = (( uparrow a) /\ the carrier of S);

        

         A3: (( id L) . a) = a;

        a <= a;

        then a in ( uparrow a) by WAYBEL_0: 18;

        then

         A4: a in X by XBOOLE_0:def 4;

        (c . a) = ( "/\" (X,L)) by Def5;

        then

         A5: (c . a) <= a by A4, YELLOW_2: 22;

        ( id L) <= c by WAYBEL_1:def 14;

        then a <= (c . a) by A3, YELLOW_2: 9;

        then

         A6: a = (c . a) by A5, ORDERS_2: 2;

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

        then a in ( rng ( closure_op S)) by A6, FUNCT_1:def 3;

        hence thesis by YELLOW_0:def 15;

      end;

      hence thesis by YELLOW_0: 57;

    end;

    theorem :: WAYBEL10:19

    

     Th19: for L be complete LATTICE holds for c be closure Function of L, L holds ( closure_op ( Image c)) = c

    proof

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

      now

        let x be Element of L;

        

         A1: ( id L) <= c by WAYBEL_1:def 14;

        x = (( id L) . x);

        then x <= (c . x) by A1, YELLOW_2: 9;

        then

         A2: (c . x) in ( uparrow x) by WAYBEL_0: 18;

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

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

        then (c . x) in (( uparrow x) /\ ( rng c)) by A2, XBOOLE_0:def 4;

        then

         A3: (c . x) >= ( "/\" ((( uparrow x) /\ ( rng c)),L)) by YELLOW_2: 22;

        (c . x) is_<=_than (( uparrow x) /\ ( rng c))

        proof

          let z be Element of L;

          assume

           A4: z in (( uparrow x) /\ ( rng c));

          then z in ( rng c) by XBOOLE_0:def 4;

          then

          consider a be object such that

           A5: a in ( dom c) and

           A6: z = (c . a) by FUNCT_1:def 3;

          reconsider a as Element of L by A5;

          z in ( uparrow x) by A4, XBOOLE_0:def 4;

          then x <= (c . a) by A6, WAYBEL_0: 18;

          then (c . x) <= (c . (c . a)) by WAYBEL_1:def 2;

          hence thesis by A6, YELLOW_2: 18;

        end;

        then

         A7: (c . x) <= ( "/\" ((( uparrow x) /\ ( rng c)),L)) by YELLOW_0: 33;

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

        

        hence (( closure_op ( Image c)) . x) = ( "/\" ((( uparrow x) /\ ( rng c)),L)) by Def5

        .= (c . x) by A3, A7, ORDERS_2: 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    registration

      let L be complete LATTICE;

      cluster ( ClImageMap L) -> one-to-one;

      coherence

      proof

        let x,y be Element of ( ClOpers L);

        reconsider a = x, b = y as closure Function of L, L by Th10;

        set f = ( ClImageMap L);

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

        

        then ( Image a) = (f . y) by Def4

        .= ( Image b) by Def4;

        

        hence x = ( closure_op ( Image b)) by Th19

        .= y by Th19;

      end;

    end

    theorem :: WAYBEL10:20

    

     Th20: for L be complete LATTICE holds (( ClImageMap L) " ) is Function of (( ClosureSystems L) opp ), ( ClOpers L)

    proof

      let L be complete LATTICE;

      set f = ( ClImageMap L);

      

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

      

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

      the carrier of (( ClosureSystems L) opp ) c= ( rng f)

      proof

        let x be object;

        assume x in the carrier of (( ClosureSystems L) opp );

        then

        reconsider x as Element of (( ClosureSystems L) opp );

        reconsider x as infs-inheriting full strict SubRelStr of L by Th16;

        

         A3: ( closure_op x) is Element of ( ClOpers L) by Th10;

        (f . ( closure_op x)) = ( Image ( closure_op x)) by Def4

        .= x by Th18;

        hence thesis by A2, A3, FUNCT_1:def 3;

      end;

      then

       A4: the carrier of (( ClosureSystems L) opp ) = ( rng f);

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

      hence thesis by A1, A4, FUNCT_2:def 1, RELSET_1: 4;

    end;

    theorem :: WAYBEL10:21

    

     Th21: for L be complete LATTICE holds for S be strict closure System of L holds ((( ClImageMap L) " ) . S) = ( closure_op S)

    proof

      let L be complete LATTICE;

      let S be infs-inheriting full strict SubRelStr of L;

      

       A1: ( closure_op S) is Element of ( ClOpers L) by Th10;

      (( ClImageMap L) . ( closure_op S)) = ( Image ( closure_op S)) by Def4

      .= S by Th18;

      hence thesis by A1, FUNCT_2: 26;

    end;

    registration

      let L be complete LATTICE;

      cluster ( ClImageMap L) -> isomorphic;

      correctness

      proof

        set f = ( ClImageMap L);

        set S = ( ClOpers L), T = (( ClosureSystems L) opp );

        reconsider g = (f " ) as Function of T, S by Th20;

        per cases ;

          case S is non empty & T is non empty;

          thus f is one-to-one;

          thus f is monotone

          proof

            let x,y be Element of S;

            reconsider c = x, d = y as closure Function of L, L by Th10;

            

             A1: (f . y) = ( Image d) by Def4;

            assume x <= y;

            then c <= d by Th12;

            then

             A2: ( Image d) is SubRelStr of ( Image c) by Th14;

            (f . x) = ( Image c) by Def4;

            then ( ~ (f . x)) >= ( ~ (f . y)) by A2, A1, Th17;

            hence (f . x) <= (f . y) by YELLOW_7: 1;

          end;

          take g;

          thus g = (f " );

          thus g is monotone

          proof

            let x,y be Element of T;

            reconsider A = ( ~ x), B = ( ~ y) as infs-inheriting full strict SubRelStr of L by Th16;

            

             A3: B = ( Image ( closure_op B)) by Th18;

            

             A4: (g . A) = ( closure_op A) by Th21;

            assume x <= y;

            then ( ~ y) <= ( ~ x) by YELLOW_7: 1;

            then

             A5: B is SubRelStr of A by Th17;

            

             A6: (g . B) = ( closure_op B) by Th21;

            A = ( Image ( closure_op A)) by Th18;

            then ( closure_op A) <= ( closure_op B) by A5, A3, Th14;

            hence (g . x) <= (g . y) by A4, A6, Th12;

          end;

        end;

          case S is empty or T is empty;

          hence thesis;

        end;

      end;

    end

    theorem :: WAYBEL10:22

    for L be complete LATTICE holds (( ClOpers L),(( ClosureSystems L) opp )) are_isomorphic

    proof

      let L be complete LATTICE;

      take ( ClImageMap L);

      thus thesis;

    end;

    begin

    theorem :: WAYBEL10:23

    

     Th23: for L be RelStr, S be full SubRelStr of L holds for X be Subset of S holds (X is directed Subset of L implies X is directed) & (X is filtered Subset of L implies X is filtered)

    proof

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

      let X be Subset of S;

      hereby

        assume

         A1: X is directed Subset of L;

        thus X is directed

        proof

          

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

          let x,y be Element of S;

          assume that

           A3: x in X and

           A4: y in X;

          x in the carrier of S by A3;

          then

          reconsider x9 = x, y9 = y as Element of L by A2;

          consider z be Element of L such that

           A5: z in X and

           A6: z >= x9 and

           A7: z >= y9 by A1, A3, A4, WAYBEL_0:def 1;

          reconsider z as Element of S by A5;

          take z;

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

        end;

      end;

      assume

       A8: X is filtered Subset of L;

      

       A9: the carrier of S c= the carrier of L by YELLOW_0:def 13;

      let x,y be Element of S;

      assume that

       A10: x in X and

       A11: y in X;

      x in the carrier of S by A10;

      then

      reconsider x9 = x, y9 = y as Element of L by A9;

      consider z be Element of L such that

       A12: z in X and

       A13: z <= x9 and

       A14: z <= y9 by A8, A10, A11, WAYBEL_0:def 2;

      reconsider z as Element of S by A12;

      take z;

      thus thesis by A12, A13, A14, YELLOW_0: 60;

    end;

    theorem :: WAYBEL10:24

    

     Th24: for L be complete LATTICE holds for S be closure System of L holds ( closure_op S) is directed-sups-preserving iff S is directed-sups-inheriting

    proof

      let L be complete LATTICE;

      let S be closure System of L;

      set c = ( closure_op S);

      

       A1: ( Image c) = the RelStr of S by Th18;

      hereby

        set Lk = { k where k be Element of L : (c . k) <= k };

        set k = the Element of L;

        

         A2: Lk c= the carrier of L

        proof

          let x be object;

          assume x in Lk;

          then ex k be Element of L st x = k & (c . k) <= k;

          hence thesis;

        end;

        (c . (c . k)) = (c . k) by YELLOW_2: 18;

        then

         A3: (c . k) in Lk;

        assume ( closure_op S) is directed-sups-preserving;

        then

         A4: ( Image c) is directed-sups-inheriting by A3, A2, WAYBEL_1: 52;

        thus S is directed-sups-inheriting

        proof

          let X be directed Subset of S such that

           A5: X <> {} and

           A6: ex_sup_of (X,L);

          reconsider Y = X as Subset of ( Image c) by A1;

          Y is directed by A1, WAYBEL_0: 3;

          hence thesis by A1, A4, A5, A6;

        end;

      end;

      assume

       A7: for X be directed Subset of S st X <> {} & ex_sup_of (X,L) holds ( "\/" (X,L)) in the carrier of S;

      let X be Subset of L such that

       A8: X is non empty directed;

      ( rng c) = the carrier of S by A1, YELLOW_0:def 15;

      then

      reconsider Y = (c .: X) as Subset of S by RELAT_1: 111;

      assume ex_sup_of (X,L);

      thus ex_sup_of ((c .: X),L) by YELLOW_0: 17;

      (c .: X) is_<=_than (c . ( sup X))

      proof

        let x be Element of L;

        assume x in (c .: X);

        then

        consider a be object such that

         A9: a in the carrier of L and

         A10: a in X and

         A11: x = (c . a) by FUNCT_2: 64;

        reconsider a as Element of L by A9;

        a <= ( sup X) by A10, YELLOW_2: 22;

        hence thesis by A11, WAYBEL_1:def 2;

      end;

      then

       A12: ( sup (c .: X)) <= (c . ( sup X)) by YELLOW_0: 32;

      X is_<=_than ( sup (c .: X))

      proof

        let x be Element of L;

        assume x in X;

        then (c . x) in (c .: X) by FUNCT_2: 35;

        then

         A13: (c . x) <= ( sup (c .: X)) by YELLOW_2: 22;

        x <= (c . x) by Th5;

        hence thesis by A13, ORDERS_2: 3;

      end;

      then

       A14: ( sup X) <= ( sup (c .: X)) by YELLOW_0: 32;

      set x = the Element of X;

      x in X by A8;

      then

       A15: (c . x) in (c .: X) by FUNCT_2: 35;

      Y is directed by A8, Th23, YELLOW_2: 15;

      then ( sup (c .: X)) in the carrier of S by A7, A15, YELLOW_0: 17;

      then ex a be Element of L st (c . a) = ( sup (c .: X)) by A1, YELLOW_2: 10;

      then (c . ( sup (c .: X))) = ( sup (c .: X)) by YELLOW_2: 18;

      then (c . ( sup X)) <= ( sup (c .: X)) by A14, WAYBEL_1:def 2;

      hence thesis by A12, ORDERS_2: 2;

    end;

    theorem :: WAYBEL10:25

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

    proof

      let L be complete LATTICE;

      let h be closure Function of L, L;

      ( closure_op ( Image h)) = h by Th19;

      hence thesis by Th24;

    end;

    registration

      let L be complete LATTICE;

      let S be directed-sups-inheriting closure System of L;

      cluster ( closure_op S) -> directed-sups-preserving;

      coherence by Th24;

    end

    registration

      let L be complete LATTICE;

      let h be directed-sups-preserving closure Function of L, L;

      cluster ( Image h) -> directed-sups-inheriting;

      coherence

      proof

        h = ( closure_op ( Image h)) by Th19;

        hence thesis by Th24;

      end;

    end

    definition

      let L be non empty reflexive RelStr;

      :: WAYBEL10:def6

      func DsupClOpers L -> non empty full strict SubRelStr of ( ClOpers L) means

      : Def6: for f be closure Function of L, L holds f is Element of it iff f is directed-sups-preserving;

      existence

      proof

        defpred P[ set] means $1 is directed-sups-preserving Function of L, L;

        set h = the directed-sups-preserving closure Function of L, L;

        h is Element of ( ClOpers L) by Def1;

        then

         A1: h in the carrier of ( ClOpers L);

        

         A2: P[h];

        consider S be non empty full strict SubRelStr of ( ClOpers L) such that

         A3: for f be Element of ( ClOpers L) holds f is Element of S iff P[f] from SubrelstrEx( A2, A1);

        take S;

        let f be closure Function of L, L;

        hereby

          assume

           A4: f is Element of S;

          then f is Element of ( ClOpers L) by YELLOW_0: 58;

          hence f is directed-sups-preserving by A3, A4;

        end;

        assume

         A5: f is directed-sups-preserving;

        f is Element of ( ClOpers L) by Def1;

        hence thesis by A3, A5;

      end;

      correctness

      proof

        defpred P[ object] means $1 is directed-sups-preserving closure Function of L, L;

        let S1,S2 be non empty full strict SubRelStr of ( ClOpers L) such that

         A6: for f be closure Function of L, L holds f is Element of S1 iff f is directed-sups-preserving and

         A7: for f be closure Function of L, L holds f is Element of S2 iff f is directed-sups-preserving;

         A8:

        now

          let f be object;

          f is Element of S2 implies f is Element of ( ClOpers L) by YELLOW_0: 58;

          then f is Element of S2 implies f is closure Function of L, L by Th10;

          hence f is Element of S2 iff P[f] by A7;

        end;

         A9:

        now

          let f be object;

          f is Element of S1 implies f is Element of ( ClOpers L) by YELLOW_0: 58;

          then f is Element of S1 implies f is closure Function of L, L by Th10;

          hence f is Element of S1 iff P[f] by A6;

        end;

         the RelStr of S1 = the RelStr of S2 from SubrelstrEq1( A9, A8);

        hence thesis;

      end;

    end

    theorem :: WAYBEL10:26

    

     Th26: for L be non empty reflexive RelStr, x be set holds x is Element of ( DsupClOpers L) iff x is directed-sups-preserving closure Function of L, L

    proof

      let L be non empty reflexive RelStr, x be set;

      x is Element of ( ClOpers L) iff x is closure Function of L, L by Th10;

      hence thesis by Def6, YELLOW_0: 58;

    end;

    definition

      let L be non empty RelStr;

      :: WAYBEL10:def7

      func Subalgebras L -> full strict non empty SubRelStr of ( ClosureSystems L) means

      : Def7: for R be strict closure System of L holds R is Element of it iff R is directed-sups-inheriting;

      existence

      proof

        defpred P[ set] means $1 is directed-sups-inheriting SubRelStr of L;

        set SL = ( subrelstr ( [#] L));

        SL is Element of ( ClosureSystems L) by Def3;

        then

         A1: SL in the carrier of ( ClosureSystems L);

        

         A2: P[SL];

        consider S be non empty full strict SubRelStr of ( ClosureSystems L) such that

         A3: for x be Element of ( ClosureSystems L) holds x is Element of S iff P[x] from SubrelstrEx( A2, A1);

        take S;

        let R be strict closure System of L;

        R is Element of ( ClosureSystems L) by Def3;

        hence thesis by A3;

      end;

      correctness

      proof

        defpred P[ object] means $1 is directed-sups-inheriting strict closure System of L;

        let S1,S2 be full strict non empty SubRelStr of ( ClosureSystems L) such that

         A4: for R be strict closure System of L holds R is Element of S1 iff R is directed-sups-inheriting and

         A5: for R be strict closure System of L holds R is Element of S2 iff R is directed-sups-inheriting;

         A6:

        now

          let x be object;

          x is Element of S2 implies x is Element of ( ClosureSystems L) by YELLOW_0: 58;

          then x is Element of S2 implies x is strict closure System of L by Th16;

          hence x is Element of S2 iff P[x] by A5;

        end;

         A7:

        now

          let x be object;

          x is Element of S1 implies x is Element of ( ClosureSystems L) by YELLOW_0: 58;

          then x is Element of S1 implies x is strict closure System of L by Th16;

          hence x is Element of S1 iff P[x] by A4;

        end;

         the RelStr of S1 = the RelStr of S2 from SubrelstrEq1( A7, A6);

        hence thesis;

      end;

    end

    theorem :: WAYBEL10:27

    

     Th27: for L be non empty RelStr, x be object holds x is Element of ( Subalgebras L) iff x is strict directed-sups-inheriting closure System of L

    proof

      let L be non empty RelStr, x be object;

      x is Element of ( ClosureSystems L) iff x is strict closure System of L by Th16;

      hence thesis by Def7, YELLOW_0: 58;

    end;

    theorem :: WAYBEL10:28

    

     Th28: for L be complete LATTICE holds ( Image (( ClImageMap L) | ( DsupClOpers L))) = (( Subalgebras L) opp )

    proof

      let L be complete LATTICE;

      defpred P[ object] means $1 is directed-sups-inheriting closure strict System of L;

       A1:

      now

        let a be object;

        hereby

          assume a is Element of ( Image (( ClImageMap L) | ( DsupClOpers L)));

          then

          consider x be Element of ( DsupClOpers L) such that

           A2: ((( ClImageMap L) | ( DsupClOpers L)) . x) = a by YELLOW_2: 10;

          reconsider x as directed-sups-preserving closure Function of L, L by Th26;

          a = (( ClImageMap L) . x) by A2, Th6

          .= ( Image x) by Def4;

          hence P[a];

        end;

        assume P[a];

        then

        reconsider S = a as directed-sups-inheriting closure strict System of L;

        reconsider x = ( closure_op S) as Element of ( DsupClOpers L) by Th26;

        S = ( Image ( closure_op S)) by Th18

        .= (( ClImageMap L) . ( closure_op S)) by Def4

        .= ((( ClImageMap L) | ( DsupClOpers L)) . x) by Th6;

        then S in ( rng (( ClImageMap L) | ( DsupClOpers L))) by FUNCT_2: 4;

        hence a is Element of ( Image (( ClImageMap L) | ( DsupClOpers L))) by YELLOW_0:def 15;

      end;

      

       A3: for a be object holds a is Element of (( Subalgebras L) opp ) iff P[a] by Th27;

       the RelStr of ( Image (( ClImageMap L) | ( DsupClOpers L))) = the RelStr of (( Subalgebras L) opp ) from SubrelstrEq1( A1, A3);

      hence thesis;

    end;

    registration

      let L be complete LATTICE;

      cluster ( corestr (( ClImageMap L) | ( DsupClOpers L))) -> isomorphic;

      coherence

      proof

        set f = ( ClImageMap L), R = ( DsupClOpers L), g = ( corestr (f | R));

        per cases ;

          case ( DsupClOpers L) is non empty & ( Image (f | R)) is non empty;

          (f | R) is one-to-one by Th7;

          hence g is one-to-one monotone by WAYBEL_1: 30;

          consider f9 be Function of (( ClosureSystems L) opp ), ( ClOpers L) such that

           A1: f9 = (f " ) and f9 is monotone by WAYBEL_0:def 38;

          reconsider h = (f9 | ( Image (f | R))) as Function of ( Image (f | R)), R by A1, Th8;

          take h;

          

          thus h = ((f | R) " ) by A1, Th8

          .= (g " ) by WAYBEL_1: 30;

          let x,y be Element of ( Image (f | R));

          reconsider a = x, b = y as Element of (( ClosureSystems L) opp ) by YELLOW_0: 58;

          reconsider A = ( ~ a), B = ( ~ b) as strict closure System of L by Th16;

          reconsider i = ( closure_op A), j = ( closure_op B) as Element of ( ClOpers L) by Th10;

          (f9 . y) = j by A1, Th21;

          then

           A2: (h . y) = j by Th6;

          assume x <= y;

          then a <= b by YELLOW_0: 59;

          then ( ~ a) >= ( ~ b) by YELLOW_7: 1;

          then

           A3: B is SubRelStr of A by Th17;

          

           A4: B = ( Image ( closure_op B)) by Th18;

          A = ( Image ( closure_op A)) by Th18;

          then ( closure_op A) <= ( closure_op B) by A3, A4, Th14;

          then

           A5: i <= j by Th12;

          (f9 . x) = i by A1, Th21;

          then (h . x) = i by Th6;

          hence (h . x) <= (h . y) by A2, A5, YELLOW_0: 60;

        end;

          case ( DsupClOpers L) is empty or ( Image (f | R)) is empty;

          hence thesis;

        end;

      end;

    end

    theorem :: WAYBEL10:29

    for L be complete LATTICE holds (( DsupClOpers L),(( Subalgebras L) opp )) are_isomorphic

    proof

      let L be complete LATTICE;

      set f = (( ClImageMap L) | ( DsupClOpers L));

      reconsider g = ( corestr f) as Function of ( DsupClOpers L), (( Subalgebras L) opp ) by Th28;

      take g;

      ( Image f) = (( Subalgebras L) opp ) by Th28;

      hence thesis;

    end;