yellow_7.miz

    begin

    notation

      let L be RelStr;

      synonym L opp for L ~ ;

    end

    theorem :: YELLOW_7:1



     Th1: for L be RelStr, x,y be Element of (L opp ) holds x <= y iff ( ~ x) >= ( ~ y)

    proof

      let L be RelStr, x,y be Element of (L opp );

      (( ~ x) ~ ) = ( ~ x) & (( ~ y) ~ ) = ( ~ y);

      hence thesis by LATTICE3: 9;

    end;

    theorem :: YELLOW_7:2



     Th2: for L be RelStr, x be Element of L, y be Element of (L opp ) holds (x <= ( ~ y) iff (x ~ ) >= y) & (x >= ( ~ y) iff (x ~ ) <= y)

    proof

      let L be RelStr, x be Element of L, y be Element of (L opp );

      ( ~ (x ~ )) = (x ~ );

      hence thesis by Th1;

    end;

    theorem :: YELLOW_7:3

    for L be RelStr holds L is empty iff (L opp ) is empty;

    theorem :: YELLOW_7:4



     Th4: for L be RelStr holds L is reflexive iff (L opp ) is reflexive

    proof

      let L be RelStr;

      thus L is reflexive implies (L opp ) is reflexive

      proof

        assume L is reflexive;

        then

         A1: the InternalRel of L is_reflexive_in the carrier of L;

        let x be object;

        assume x in the carrier of (L opp );

        then [x, x] in the InternalRel of L by A1;

        hence thesis by RELAT_1:def 7;

      end;

      assume (L opp ) is reflexive;

      then

       A2: the InternalRel of (L opp ) is_reflexive_in the carrier of (L opp );

      let x be object;

      assume x in the carrier of L;

      then [x, x] in the InternalRel of (L opp ) by A2;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: YELLOW_7:5



     Th5: for L be RelStr holds L is antisymmetric iff (L opp ) is antisymmetric

    proof

      let L be RelStr;

      thus L is antisymmetric implies (L opp ) is antisymmetric

      proof

        assume

         A1: L is antisymmetric;

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

        assume x <= y & x >= y;

        then ( ~ x) >= ( ~ y) & ( ~ x) <= ( ~ y) by Th1;

        hence thesis by A1;

      end;

      assume

       A2: (L opp ) is antisymmetric;

      let x,y be Element of L;

      assume x <= y & x >= y;

      then (x ~ ) >= (y ~ ) & (x ~ ) <= (y ~ ) by LATTICE3: 9;

      hence thesis by A2;

    end;

    theorem :: YELLOW_7:6



     Th6: for L be RelStr holds L is transitive iff (L opp ) is transitive

    proof

      let L be RelStr;

      thus L is transitive implies (L opp ) is transitive

      proof

        assume

         A1: L is transitive;

        let x,y,z be Element of (L opp );

        assume x <= y & z >= y;

        then ( ~ x) >= ( ~ y) & ( ~ z) <= ( ~ y) by Th1;

        hence thesis by Th1, A1;

      end;

      assume

       A2: (L opp ) is transitive;

      let x,y,z be Element of L;

      assume x <= y & z >= y;

      then (x ~ ) >= (y ~ ) & (z ~ ) <= (y ~ ) by LATTICE3: 9;

      then (x ~ ) >= (z ~ ) by A2;

      hence thesis by LATTICE3: 9;

    end;

    theorem :: YELLOW_7:7



     Th7: for L be non empty RelStr holds L is connected iff (L opp ) is connected

    proof

      let L be non empty RelStr;

      thus L is connected implies (L opp ) is connected

      proof

        assume

         A1: for x,y be Element of L holds x <= y or x >= y;

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

        ( ~ x) <= ( ~ y) or ( ~ x) >= ( ~ y) by A1;

        hence thesis by Th1;

      end;

      assume

       A2: for x,y be Element of (L opp ) holds x <= y or x >= y;

      let x,y be Element of L;

      (x ~ ) <= (y ~ ) or (x ~ ) >= (y ~ ) by A2;

      hence thesis by LATTICE3: 9;

    end;

    registration

      let L be reflexive RelStr;

      cluster (L opp ) -> reflexive;

      coherence by Th4;

    end

    registration

      let L be transitive RelStr;

      cluster (L opp ) -> transitive;

      coherence by Th6;

    end

    registration

      let L be antisymmetric RelStr;

      cluster (L opp ) -> antisymmetric;

      coherence by Th5;

    end

    registration

      let L be connected non empty RelStr;

      cluster (L opp ) -> connected;

      coherence by Th7;

    end

    theorem :: YELLOW_7:8



     Th8: for L be RelStr, x be Element of L, X be set holds (x is_<=_than X iff (x ~ ) is_>=_than X) & (x is_>=_than X iff (x ~ ) is_<=_than X)

    proof

      let L be RelStr, x be Element of L, X be set;

       A1:

      now

        let L be RelStr, x be Element of L, X be set;

        assume

         A2: x is_<=_than X;

        thus (x ~ ) is_>=_than X

        proof

          let a be Element of (L opp );

          assume a in X;

          then (( ~ a) ~ ) = ( ~ a) & x <= ( ~ a) by A2;

          hence thesis by LATTICE3: 9;

        end;

      end;

       A3:

      now

        let L be RelStr, x be Element of L, X be set;

        assume

         A4: x is_>=_than X;

        thus (x ~ ) is_<=_than X

        proof

          let a be Element of (L opp );

          assume a in X;

          then (( ~ a) ~ ) = ( ~ a) & x >= ( ~ a) by A4;

          hence thesis by LATTICE3: 9;

        end;

      end;

      ((x ~ ) ~ ) is_<=_than X implies x is_<=_than X by YELLOW_0: 2;

      hence x is_<=_than X iff (x ~ ) is_>=_than X by A1, A3;

      ((x ~ ) ~ ) is_>=_than X implies x is_>=_than X by YELLOW_0: 2;

      hence thesis by A1, A3;

    end;

    theorem :: YELLOW_7:9



     Th9: for L be RelStr, x be Element of (L opp ), X be set holds (x is_<=_than X iff ( ~ x) is_>=_than X) & (x is_>=_than X iff ( ~ x) is_<=_than X)

    proof

      let L be RelStr, x be Element of (L opp ), X be set;

      (( ~ x) ~ ) = ( ~ x);

      hence thesis by Th8;

    end;

    theorem :: YELLOW_7:10



     Th10: for L be RelStr, X be set holds ex_sup_of (X,L) iff ex_inf_of (X,(L opp ))

    proof

      let L be RelStr, X be set;

      hereby

        assume ex_sup_of (X,L);

        then

        consider a be Element of L such that

         A1: X is_<=_than a and

         A2: for b be Element of L st X is_<=_than b holds b >= a and

         A3: for c be Element of L st X is_<=_than c & for b be Element of L st X is_<=_than b holds b >= c holds c = a;

        thus ex_inf_of (X,(L opp ))

        proof

          take (a ~ );

          thus X is_>=_than (a ~ ) by A1, Th8;

          hereby

            let b be Element of (L opp );

            assume X is_>=_than b;

            then X is_<=_than ( ~ b) by Th9;

            hence b <= (a ~ ) by Th2, A2;

          end;

          let c be Element of (L opp );

          assume X is_>=_than c;

          then

           A4: X is_<=_than ( ~ c) by Th9;

          assume

           A5: for b be Element of (L opp ) st X is_>=_than b holds b <= c;

          now

            let b be Element of L;

            assume X is_<=_than b;

            then X is_>=_than (b ~ ) by Th8;

            hence b >= ( ~ c) by Th2, A5;

          end;

          hence thesis by A3, A4;

        end;

      end;

      assume ex_inf_of (X,(L opp ));

      then

      consider a be Element of (L opp ) such that

       A6: X is_>=_than a and

       A7: for b be Element of (L opp ) st X is_>=_than b holds b <= a and

       A8: for c be Element of (L opp ) st X is_>=_than c & for b be Element of (L opp ) st X is_>=_than b holds b <= c holds c = a;

      take ( ~ a);

      thus X is_<=_than ( ~ a) by A6, Th9;

      hereby

        let b be Element of L;

        assume X is_<=_than b;

        then X is_>=_than (b ~ ) by Th8;

        hence b >= ( ~ a) by Th2, A7;

      end;

      let c be Element of L;

      assume X is_<=_than c;

      then

       A9: X is_>=_than (c ~ ) by Th8;

      assume

       A10: for b be Element of L st X is_<=_than b holds b >= c;

      now

        let b be Element of (L opp );

        assume X is_>=_than b;

        then X is_<=_than ( ~ b) by Th9;

        hence b <= (c ~ ) by Th2, A10;

      end;

      hence thesis by A8, A9;

    end;

    theorem :: YELLOW_7:11



     Th11: for L be RelStr, X be set holds ex_sup_of (X,(L opp )) iff ex_inf_of (X,L)

    proof

      let L be RelStr, X be set;

       ex_inf_of (X,L) iff ex_inf_of (X,((L opp ) ~ )) by YELLOW_0: 14;

      hence thesis by Th10;

    end;

    theorem :: YELLOW_7:12



     Th12: for L be non empty RelStr, X be set st ex_sup_of (X,L) or ex_inf_of (X,(L opp )) holds ( "\/" (X,L)) = ( "/\" (X,(L opp )))

    proof

      let L be non empty RelStr, X be set;

      assume

       A1: ex_sup_of (X,L) or ex_inf_of (X,(L opp ));

      then

       A2: ex_sup_of (X,L) by Th10;

      then ( "\/" (X,L)) is_>=_than X by YELLOW_0:def 9;

      then

       A3: (( "\/" (X,L)) ~ ) is_<=_than X by Th8;

       A4:

      now

        let x be Element of (L opp );

        assume x is_<=_than X;

        then ( ~ x) is_>=_than X by Th9;

        then ( ~ x) >= ( "\/" (X,L)) by A2, YELLOW_0:def 9;

        hence x <= (( "\/" (X,L)) ~ ) by Th2;

      end;

       ex_inf_of (X,(L opp )) by A1, Th10;

      hence thesis by A3, A4, YELLOW_0:def 10;

    end;

    theorem :: YELLOW_7:13



     Th13: for L be non empty RelStr, X be set st ex_inf_of (X,L) or ex_sup_of (X,(L opp )) holds ( "/\" (X,L)) = ( "\/" (X,(L opp )))

    proof

      let L be non empty RelStr, X be set;

      assume

       A1: ex_inf_of (X,L) or ex_sup_of (X,(L opp ));

      then

       A2: ex_inf_of (X,L) by Th11;

      then ( "/\" (X,L)) is_<=_than X by YELLOW_0:def 10;

      then

       A3: (( "/\" (X,L)) ~ ) is_>=_than X by Th8;

       A4:

      now

        let x be Element of (L opp );

        assume x is_>=_than X;

        then ( ~ x) is_<=_than X by Th9;

        then ( ~ x) <= ( "/\" (X,L)) by A2, YELLOW_0:def 10;

        hence x >= (( "/\" (X,L)) ~ ) by Th2;

      end;

       ex_sup_of (X,(L opp )) by A1, Th11;

      hence thesis by A3, A4, YELLOW_0:def 9;

    end;

    theorem :: YELLOW_7:14



     Th14: for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is with_infima holds L2 is with_infima

    proof

      let L1,L2 be RelStr such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: for x,y be Element of L1 holds ex z be Element of L1 st z <= x & z <= y & for z9 be Element of L1 st z9 <= x & z9 <= y holds z9 <= z;

      let a,b be Element of L2;

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

      consider z be Element of L1 such that

       A3: z <= x & z <= y and

       A4: for z9 be Element of L1 st z9 <= x & z9 <= y holds z9 <= z by A2;

      reconsider c = z as Element of L2 by A1;

      take c;

      thus c <= a & c <= b by A1, A3;

      let d be Element of L2;

      reconsider z9 = d as Element of L1 by A1;

      assume d <= a & d <= b;

      then z9 <= x & z9 <= y by A1;

      then z9 <= z by A4;

      hence thesis by A1;

    end;

    theorem :: YELLOW_7:15

    for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is with_suprema holds L2 is with_suprema

    proof

      let L1,L2 be RelStr such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: for x,y be Element of L1 holds ex z be Element of L1 st z >= x & z >= y & for z9 be Element of L1 st z9 >= x & z9 >= y holds z9 >= z;

      let a,b be Element of L2;

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

      consider z be Element of L1 such that

       A3: z >= x & z >= y and

       A4: for z9 be Element of L1 st z9 >= x & z9 >= y holds z9 >= z by A2;

      reconsider c = z as Element of L2 by A1;

      take c;

      thus c >= a & c >= b by A1, A3;

      let d be Element of L2;

      reconsider z9 = d as Element of L1 by A1;

      assume d >= a & d >= b;

      then z9 >= x & z9 >= y by A1;

      then z9 >= z by A4;

      hence thesis by A1;

    end;

    theorem :: YELLOW_7:16



     Th16: for L be RelStr holds L is with_infima iff (L opp ) is with_suprema

    proof

      let L be RelStr;

      L is with_infima iff ((L opp ) ~ ) is with_infima by Th14;

      hence thesis by LATTICE3: 10;

    end;

    theorem :: YELLOW_7:17



     Th17: for L be non empty RelStr holds L is complete iff (L opp ) is complete

    proof

      let L be non empty RelStr;

       A1:

      now

        let L be non empty RelStr;

        assume

         A2: L is complete;

        thus (L opp ) is complete

        proof

          let X be set;

          set Y = { x where x be Element of L : x is_<=_than X };

          consider a be Element of L such that

           A3: Y is_<=_than a and

           A4: for b be Element of L st Y is_<=_than b holds a <= b by A2;

          take x = (a ~ );

          thus X is_<=_than x

          proof

            let y be Element of (L opp );

            assume

             A5: y in X;

            Y is_<=_than ( ~ y)

            proof

              let b be Element of L;

              assume b in Y;

              then ex z be Element of L st b = z & z is_<=_than X;

              hence thesis by A5;

            end;

            hence thesis by Th2, A4;

          end;

          let y be Element of (L opp );

          assume X is_<=_than y;

          then X is_>=_than ( ~ y) by Th9;

          then ( ~ y) in Y;

          then

           A6: a >= ( ~ y) by A3;

          ( ~ x) = x;

          hence thesis by A6, Th1;

        end;

      end;

      ((L opp ) ~ ) is complete implies L is complete by YELLOW_0: 3;

      hence thesis by A1;

    end;

    registration

      let L be with_infima RelStr;

      cluster (L opp ) -> with_suprema;

      coherence by Th16;

    end

    registration

      let L be with_suprema RelStr;

      cluster (L opp ) -> with_infima;

      coherence by LATTICE3: 10;

    end

    registration

      let L be complete non empty RelStr;

      cluster (L opp ) -> complete;

      coherence by Th17;

    end

    theorem :: YELLOW_7:18

    for L be non empty RelStr holds for X be Subset of L, Y be Subset of (L opp ) st X = Y holds ( fininfs X) = ( finsups Y) & ( finsups X) = ( fininfs Y)

    proof

      let L be non empty RelStr;

      let X be Subset of L, Y be Subset of (L opp ) such that

       A1: X = Y;

      thus ( fininfs X) c= ( finsups Y)

      proof

        let x be object;

        assume x in ( fininfs X);

        then

        consider Z be finite Subset of X such that

         A2: x = ( "/\" (Z,L)) & ex_inf_of (Z,L);

        x = ( "\/" (Z,(L opp ))) & ex_sup_of (Z,(L opp )) by A2, Th11, Th13;

        hence thesis by A1;

      end;

      thus ( finsups Y) c= ( fininfs X)

      proof

        let x be object;

        assume x in ( finsups Y);

        then

        consider Z be finite Subset of Y such that

         A3: x = ( "\/" (Z,(L opp ))) & ex_sup_of (Z,(L opp ));

        x = ( "/\" (Z,L)) & ex_inf_of (Z,L) by A3, Th11, Th13;

        hence thesis by A1;

      end;

      thus ( finsups X) c= ( fininfs Y)

      proof

        let x be object;

        assume x in ( finsups X);

        then

        consider Z be finite Subset of X such that

         A4: x = ( "\/" (Z,L)) & ex_sup_of (Z,L);

        x = ( "/\" (Z,(L opp ))) & ex_inf_of (Z,(L opp )) by A4, Th10, Th12;

        hence thesis by A1;

      end;

      let x be object;

      assume x in ( fininfs Y);

      then

      consider Z be finite Subset of Y such that

       A5: x = ( "/\" (Z,(L opp ))) & ex_inf_of (Z,(L opp ));

      x = ( "\/" (Z,L)) & ex_sup_of (Z,L) by A5, Th10, Th12;

      hence thesis by A1;

    end;

    theorem :: YELLOW_7:19



     Th19: for L be RelStr holds for X be Subset of L, Y be Subset of (L opp ) st X = Y holds ( downarrow X) = ( uparrow Y) & ( uparrow X) = ( downarrow Y)

    proof

      let L be RelStr;

      let X be Subset of L, Y be Subset of (L opp ) such that

       A1: X = Y;

      thus ( downarrow X) c= ( uparrow Y)

      proof

        let x be object;

        assume

         A2: x in ( downarrow X);

        then

        reconsider x as Element of L;

        consider y be Element of L such that

         A3: y >= x and

         A4: y in X by A2, WAYBEL_0:def 15;

        (y ~ ) <= (x ~ ) by A3, LATTICE3: 9;

        hence thesis by A1, A4, WAYBEL_0:def 16;

      end;

      thus ( uparrow Y) c= ( downarrow X)

      proof

        let x be object;

        assume

         A5: x in ( uparrow Y);

        then

        reconsider x as Element of (L opp );

        consider y be Element of (L opp ) such that

         A6: y <= x and

         A7: y in Y by A5, WAYBEL_0:def 16;

        ( ~ y) >= ( ~ x) by A6, Th1;

        hence thesis by A1, A7, WAYBEL_0:def 15;

      end;

      thus ( uparrow X) c= ( downarrow Y)

      proof

        let x be object;

        assume

         A8: x in ( uparrow X);

        then

        reconsider x as Element of L;

        consider y be Element of L such that

         A9: y <= x and

         A10: y in X by A8, WAYBEL_0:def 16;

        (y ~ ) >= (x ~ ) by A9, LATTICE3: 9;

        hence thesis by A1, A10, WAYBEL_0:def 15;

      end;

      let x be object;

      assume

       A11: x in ( downarrow Y);

      then

      reconsider x as Element of (L opp );

      consider y be Element of (L opp ) such that

       A12: y >= x and

       A13: y in Y by A11, WAYBEL_0:def 15;

      ( ~ y) <= ( ~ x) by A12, Th1;

      hence thesis by A1, A13, WAYBEL_0:def 16;

    end;

    theorem :: YELLOW_7:20

    for L be non empty RelStr holds for x be Element of L, y be Element of (L opp ) st x = y holds ( downarrow x) = ( uparrow y) & ( uparrow x) = ( downarrow y) by Th19;

    theorem :: YELLOW_7:21



     Th21: for L be with_infima Poset, x,y be Element of L holds (x "/\" y) = ((x ~ ) "\/" (y ~ ))

    proof

      let L be with_infima Poset, x,y be Element of L;

      (x "/\" y) <= y by YELLOW_0: 23;

      then

       A1: ((x "/\" y) ~ ) >= (y ~ ) by LATTICE3: 9;



       A2: ( ~ (x ~ )) = (x ~ ) & ( ~ (y ~ )) = (y ~ );

       A3:

      now

        let d be Element of (L opp );

        assume d >= (x ~ ) & d >= (y ~ );

        then ( ~ d) <= x & ( ~ d) <= y by A2, Th1;

        then

         A4: ( ~ d) <= (x "/\" y) by YELLOW_0: 23;

        (( ~ d) ~ ) = ( ~ d);

        hence ((x "/\" y) ~ ) <= d by A4, LATTICE3: 9;

      end;

      (x "/\" y) <= x by YELLOW_0: 23;

      then ((x "/\" y) ~ ) >= (x ~ ) by LATTICE3: 9;

      hence thesis by A1, A3, YELLOW_0: 22;

    end;

    theorem :: YELLOW_7:22



     Th22: for L be with_infima Poset, x,y be Element of (L opp ) holds (( ~ x) "/\" ( ~ y)) = (x "\/" y)

    proof

      let L be with_infima Poset, x,y be Element of (L opp );

      (( ~ x) ~ ) = ( ~ x) & (( ~ y) ~ ) = ( ~ y);

      hence thesis by Th21;

    end;

    theorem :: YELLOW_7:23



     Th23: for L be with_suprema Poset, x,y be Element of L holds (x "\/" y) = ((x ~ ) "/\" (y ~ ))

    proof

      let L be with_suprema Poset, x,y be Element of L;

      (x "\/" y) >= y by YELLOW_0: 22;

      then

       A1: ((x "\/" y) ~ ) <= (y ~ ) by LATTICE3: 9;



       A2: ( ~ (x ~ )) = (x ~ ) & ( ~ (y ~ )) = (y ~ );

       A3:

      now

        let d be Element of (L opp );

        assume d <= (x ~ ) & d <= (y ~ );

        then ( ~ d) >= x & ( ~ d) >= y by A2, Th1;

        then

         A4: ( ~ d) >= (x "\/" y) by YELLOW_0: 22;

        (( ~ d) ~ ) = ( ~ d);

        hence ((x "\/" y) ~ ) >= d by A4, LATTICE3: 9;

      end;

      (x "\/" y) >= x by YELLOW_0: 22;

      then ((x "\/" y) ~ ) <= (x ~ ) by LATTICE3: 9;

      hence thesis by A1, A3, YELLOW_0: 23;

    end;

    theorem :: YELLOW_7:24



     Th24: for L be with_suprema Poset, x,y be Element of (L opp ) holds (( ~ x) "\/" ( ~ y)) = (x "/\" y)

    proof

      let L be with_suprema Poset, x,y be Element of (L opp );

      (( ~ x) ~ ) = ( ~ x) & (( ~ y) ~ ) = ( ~ y);

      hence thesis by Th23;

    end;

    theorem :: YELLOW_7:25



     Th25: for L be LATTICE holds L is distributive iff (L opp ) is distributive

    proof

      let L be LATTICE;

      hereby

        assume

         A1: L is distributive;

        thus (L opp ) is distributive

        proof

          let x,y,z be Element of (L opp );



          thus (x "/\" (y "\/" z)) = (( ~ x) "\/" ( ~ (y "\/" z))) by Th24

          .= (( ~ x) "\/" (( ~ y) "/\" ( ~ z))) by Th22

          .= ((( ~ x) "\/" ( ~ y)) "/\" (( ~ x) "\/" ( ~ z))) by A1, WAYBEL_1: 5

          .= (( ~ (x "/\" y)) "/\" (( ~ x) "\/" ( ~ z))) by Th24

          .= (( ~ (x "/\" y)) "/\" ( ~ (x "/\" z))) by Th24

          .= ((x "/\" y) "\/" (x "/\" z)) by Th22;

        end;

      end;

      assume

       A2: (L opp ) is distributive;

      let x,y,z be Element of L;



      thus (x "/\" (y "\/" z)) = ((x ~ ) "\/" ((y "\/" z) ~ )) by Th21

      .= ((x ~ ) "\/" ((y ~ ) "/\" (z ~ ))) by Th23

      .= (((x ~ ) "\/" (y ~ )) "/\" ((x ~ ) "\/" (z ~ ))) by A2, WAYBEL_1: 5

      .= (((x "/\" y) ~ ) "/\" ((x ~ ) "\/" (z ~ ))) by Th21

      .= (((x "/\" y) ~ ) "/\" ((x "/\" z) ~ )) by Th21

      .= ((x "/\" y) "\/" (x "/\" z)) by Th23;

    end;

    registration

      let L be distributive LATTICE;

      cluster (L opp ) -> distributive;

      coherence by Th25;

    end

    theorem :: YELLOW_7:26



     Th26: for L be RelStr, x be set holds x is directed Subset of L iff x is filtered Subset of (L opp )

    proof

      let L be RelStr, x be set;

      hereby

        assume x is directed Subset of L;

        then

        reconsider X = x as directed Subset of L;

        reconsider Y = X as Subset of (L opp );

        Y is filtered

        proof

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

          assume x in Y & y in Y;

          then

          consider z be Element of L such that

           A1: z in X & z >= ( ~ x) & z >= ( ~ y) by WAYBEL_0:def 1;

          take (z ~ );

          ( ~ (z ~ )) = (z ~ );

          hence thesis by A1, Th1;

        end;

        hence x is filtered Subset of (L opp );

      end;

      assume x is filtered Subset of (L opp );

      then

      reconsider X = x as filtered Subset of (L opp );

      reconsider Y = X as Subset of L;

      Y is directed

      proof

        let x,y be Element of L;

        assume x in Y & y in Y;

        then

        consider z be Element of (L opp ) such that

         A2: z in X & z <= (x ~ ) & z <= (y ~ ) by WAYBEL_0:def 2;

        take ( ~ z);

        (( ~ z) ~ ) = ( ~ z);

        hence thesis by A2, LATTICE3: 9;

      end;

      hence thesis;

    end;

    theorem :: YELLOW_7:27

    for L be RelStr, x be set holds x is directed Subset of (L opp ) iff x is filtered Subset of L

    proof

      let L be RelStr, x be set;

      x is filtered Subset of L iff x is filtered Subset of ((L opp ) ~ ) by WAYBEL_0: 4;

      hence thesis by Th26;

    end;

    theorem :: YELLOW_7:28



     Th28: for L be RelStr, x be set holds x is lower Subset of L iff x is upper Subset of (L opp )

    proof

      let L be RelStr, x be set;

      hereby

        assume x is lower Subset of L;

        then

        reconsider X = x as lower Subset of L;

        reconsider Y = X as Subset of (L opp );

        Y is upper

        proof

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

          assume that

           A1: x in Y and

           A2: x <= y;

          ( ~ x) >= ( ~ y) by A2, Th1;

          hence thesis by A1, WAYBEL_0:def 19;

        end;

        hence x is upper Subset of (L opp );

      end;

      assume x is upper Subset of (L opp );

      then

      reconsider X = x as upper Subset of (L opp );

      reconsider Y = X as Subset of L;

      Y is lower

      proof

        let x,y be Element of L;

        assume that

         A3: x in Y and

         A4: x >= y;

        (x ~ ) <= (y ~ ) by A4, LATTICE3: 9;

        hence thesis by A3, WAYBEL_0:def 20;

      end;

      hence thesis;

    end;

    theorem :: YELLOW_7:29

    for L be RelStr, x be set holds x is lower Subset of (L opp ) iff x is upper Subset of L

    proof

      let L be RelStr, x be set;

      x is upper Subset of L iff x is upper Subset of ((L opp ) ~ ) by WAYBEL_0: 25;

      hence thesis by Th28;

    end;

    theorem :: YELLOW_7:30



     Th30: for L be RelStr holds L is lower-bounded iff (L opp ) is upper-bounded

    proof

      let L be RelStr;

      thus L is lower-bounded implies (L opp ) is upper-bounded

      proof

        given x be Element of L such that

         A1: x is_<=_than the carrier of L;

        take (x ~ );

        thus thesis by A1, Th8;

      end;

      given x be Element of (L opp ) such that

       A2: x is_>=_than the carrier of (L opp );

      take ( ~ x);

      thus thesis by A2, Th9;

    end;

    theorem :: YELLOW_7:31



     Th31: for L be RelStr holds (L opp ) is lower-bounded iff L is upper-bounded

    proof

      let L be RelStr;

      thus (L opp ) is lower-bounded implies L is upper-bounded

      proof

        given x be Element of (L opp ) such that

         A1: x is_<=_than the carrier of (L opp );

        take ( ~ x);

        thus thesis by A1, Th9;

      end;

      given x be Element of L such that

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

      take (x ~ );

      thus thesis by A2, Th8;

    end;

    theorem :: YELLOW_7:32

    for L be RelStr holds L is bounded iff (L opp ) is bounded by Th30, Th31;

    theorem :: YELLOW_7:33

    for L be lower-bounded antisymmetric non empty RelStr holds (( Bottom L) ~ ) = ( Top (L opp )) & ( ~ ( Top (L opp ))) = ( Bottom L) by Th12, YELLOW_0: 42;

    theorem :: YELLOW_7:34

    for L be upper-bounded antisymmetric non empty RelStr holds (( Top L) ~ ) = ( Bottom (L opp )) & ( ~ ( Bottom (L opp ))) = ( Top L) by Th13, YELLOW_0: 43;

    theorem :: YELLOW_7:35



     Th35: for L be bounded LATTICE, x,y be Element of L holds y is_a_complement_of x iff (y ~ ) is_a_complement_of (x ~ )

    proof

      let L be bounded LATTICE, x,y be Element of L;

      hereby

        assume

         A1: y is_a_complement_of x;



        then

         A2: ((x ~ ) "\/" (y ~ )) = (( Bottom L) ~ ) by Th21

        .= ( Top (L opp )) by Th12, YELLOW_0: 42;

        ((x ~ ) "/\" (y ~ )) = (( Top L) ~ ) by Th23, A1

        .= ( Bottom (L opp )) by Th13, YELLOW_0: 43;

        hence (y ~ ) is_a_complement_of (x ~ ) by A2;

      end;

      assume that

       A3: ((x ~ ) "\/" (y ~ )) = ( Top (L opp )) and

       A4: ((x ~ ) "/\" (y ~ )) = ( Bottom (L opp ));



      thus (x "\/" y) = ((x ~ ) "/\" (y ~ )) by Th23

      .= ( Top L) by A4, Th13, YELLOW_0: 43;



      thus (x "/\" y) = ((x ~ ) "\/" (y ~ )) by Th21

      .= ( Bottom L) by A3, Th12, YELLOW_0: 42;

    end;

    theorem :: YELLOW_7:36



     Th36: for L be bounded LATTICE holds L is complemented iff (L opp ) is complemented

    proof

      let L be bounded LATTICE;

      thus L is complemented implies (L opp ) is complemented

      proof

        assume

         A1: for x be Element of L holds ex y be Element of L st y is_a_complement_of x;

        let x be Element of (L opp );

        consider y be Element of L such that

         A2: y is_a_complement_of ( ~ x) by A1;

        take (y ~ );

        (( ~ x) ~ ) = ( ~ x);

        hence thesis by A2, Th35;

      end;

      assume

       A3: for x be Element of (L opp ) holds ex y be Element of (L opp ) st y is_a_complement_of x;

      let x be Element of L;

      consider y be Element of (L opp ) such that

       A4: y is_a_complement_of (x ~ ) by A3;

      take ( ~ y);

      (( ~ y) ~ ) = ( ~ y);

      hence thesis by A4, Th35;

    end;

    registration

      let L be lower-bounded RelStr;

      cluster (L opp ) -> upper-bounded;

      coherence by Th30;

    end

    registration

      let L be upper-bounded RelStr;

      cluster (L opp ) -> lower-bounded;

      coherence by Th31;

    end

    registration

      let L be complemented bounded LATTICE;

      cluster (L opp ) -> complemented;

      coherence by Th36;

    end

    theorem :: YELLOW_7:37

    for L be Boolean LATTICE, x be Element of L holds ( 'not' (x ~ )) = ( 'not' x)

    proof

      let L be Boolean LATTICE, x be Element of L;

      for x be Element of L holds ( 'not' ( 'not' x)) = x by WAYBEL_1: 87;

      then ( 'not' x) is_a_complement_of x by WAYBEL_1: 86;

      then (( 'not' x) ~ ) is_a_complement_of (x ~ ) by Th35;

      hence thesis by YELLOW_5: 11;

    end;

    definition

      let L be non empty RelStr;

      :: YELLOW_7:def1

      func ComplMap L -> Function of L, (L opp ) means

      : Def1: for x be Element of L holds (it . x) = ( 'not' x);

      existence

      proof

        deffunc N( Element of L) = ( 'not' $1);

        consider f be Function of L, L such that

         A1: for x be Element of L holds (f . x) = N(x) from FUNCT_2:sch 4;

        reconsider f as Function of L, (L opp );

        take f;

        thus thesis by A1;

      end;

      correctness

      proof

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

         A2: not thesis;

        now

          let x be Element of L;



          thus (f1 . x) = ( 'not' x) by A2

          .= (f2 . x) by A2;

        end;

        hence thesis by A2, FUNCT_2: 63;

      end;

    end

    registration

      let L be Boolean LATTICE;

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

      coherence

      proof

        let a,b be Element of L;

        set f = ( ComplMap L);



         A1: ( 'not' ( 'not' a)) = a by WAYBEL_1: 87;

        (f . a) = ( 'not' a) & (f . b) = ( 'not' b) by Def1;

        hence thesis by A1, WAYBEL_1: 87;

      end;

    end

    registration

      let L be Boolean LATTICE;

      cluster ( ComplMap L) -> isomorphic;

      coherence

      proof

        set f = ( ComplMap L);



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



         A2: ( rng f) = the carrier of (L opp )

        proof

          thus ( rng f) c= the carrier of (L opp );

          let x be object;

          assume x in the carrier of (L opp );

          then

          reconsider x as Element of L;

          x = ( 'not' ( 'not' x)) by WAYBEL_1: 87;

          then (f . ( 'not' x)) = x by Def1;

          hence thesis by A1, FUNCT_1:def 3;

        end;

        now

          let x,y be Element of L;

          (f . x) = (( 'not' x) ~ ) & (f . y) = (( 'not' y) ~ ) by Def1;

          then

           A3: ( 'not' x) >= ( 'not' y) iff (f . x) <= (f . y) by LATTICE3: 9;

          x = ( 'not' ( 'not' x)) & y = ( 'not' ( 'not' y)) by WAYBEL_1: 87;

          hence x <= y iff (f . x) <= (f . y) by A3, WAYBEL_1: 83;

        end;

        hence thesis by A2, WAYBEL_0: 66;

      end;

    end

    theorem :: YELLOW_7:38

    for L be Boolean LATTICE holds (L,(L opp )) are_isomorphic

    proof

      let L be Boolean LATTICE;

      take ( ComplMap L);

      thus thesis;

    end;

    theorem :: YELLOW_7:39

    for S,T be non empty RelStr, f be set holds (f is Function of S, T iff f is Function of (S opp ), T) & (f is Function of S, T iff f is Function of S, (T opp )) & (f is Function of S, T iff f is Function of (S opp ), (T opp ));

    theorem :: YELLOW_7:40

    for S,T be non empty RelStr holds for f be Function of S, T, g be Function of S, (T opp ) st f = g holds (f is monotone iff g is antitone) & (f is antitone iff g is monotone)

    proof

      let S,T be non empty RelStr;

      let f be Function of S, T, g be Function of S, (T ~ ) such that

       A1: f = g;

      thus f is monotone implies g is antitone

      proof

        assume

         A2: for x,y be Element of S st x <= y holds (f . x) <= (f . y);

        let x,y be Element of S;

        assume x <= y;

        then

         A3: (f . x) <= (f . y) by A2;

        ((f . x) ~ ) = (f . x) & ((f . y) ~ ) = (f . y);

        hence thesis by A1, A3, LATTICE3: 9;

      end;

      thus g is antitone implies f is monotone

      proof

        assume

         A4: for x,y be Element of S st x <= y holds for a,b be Element of (T opp ) st a = (g . x) & b = (g . y) holds a >= b;

        let x,y be Element of S;

        assume x <= y;

        then

         A5: (g . y) <= (g . x) by A4;

        ( ~ (g . x)) = (g . x) & ( ~ (g . y)) = (g . y);

        hence thesis by A1, A5, Th1;

      end;

      thus f is antitone implies g is monotone

      proof

        assume

         A6: for x,y be Element of S st x <= y holds for a,b be Element of T st a = (f . x) & b = (f . y) holds a >= b;

        let x,y be Element of S;

        assume x <= y;

        then

         A7: (f . y) <= (f . x) by A6;

        ((f . x) ~ ) = (f . x) & ((f . y) ~ ) = (f . y);

        hence thesis by A1, A7, LATTICE3: 9;

      end;

      thus g is monotone implies f is antitone

      proof

        assume

         A8: for x,y be Element of S st x <= y holds (g . x) <= (g . y);

        let x,y be Element of S;

        assume x <= y;

        then

         A9: (g . y) >= (g . x) by A8;

        ( ~ (g . x)) = (g . x) & ( ~ (g . y)) = (g . y);

        hence thesis by A1, A9, Th1;

      end;

    end;

    theorem :: YELLOW_7:41

    for S,T be non empty RelStr holds for f be Function of S, (T opp ), g be Function of (S opp ), T st f = g holds (f is monotone iff g is monotone) & (f is antitone iff g is antitone)

    proof

      let S,T be non empty RelStr;

      let f be Function of S, (T ~ ), g be Function of (S ~ ), T such that

       A1: f = g;

      thus f is monotone implies g is monotone

      proof

        assume

         A2: for x,y be Element of S st x <= y holds (f . x) <= (f . y);

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

        assume x <= y;

        then ( ~ y) <= ( ~ x) by Th1;

        then

         A3: (f . ( ~ y)) <= (f . ( ~ x)) by A2;

        ( ~ (f . ( ~ x))) = (f . ( ~ x)) & ( ~ (f . ( ~ y))) = (f . ( ~ y));

        hence thesis by A1, A3, Th1;

      end;

      thus g is monotone implies f is monotone

      proof

        assume

         A4: for x,y be Element of (S opp ) st x <= y holds (g . x) <= (g . y);

        let x,y be Element of S;

        assume x <= y;

        then (y ~ ) <= (x ~ ) by LATTICE3: 9;

        then

         A5: (g . (y ~ )) <= (g . (x ~ )) by A4;

        ((g . (x ~ )) ~ ) = (g . (x ~ )) & ((g . (y ~ )) ~ ) = (g . (y ~ ));

        hence thesis by A1, A5, LATTICE3: 9;

      end;

      thus f is antitone implies g is antitone

      proof

        assume

         A6: for x,y be Element of S st x <= y holds for a,b be Element of (T ~ ) st a = (f . x) & b = (f . y) holds a >= b;

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

        assume x <= y;

        then ( ~ y) <= ( ~ x) by Th1;

        then

         A7: (f . ( ~ y)) >= (f . ( ~ x)) by A6;

        ( ~ (f . ( ~ x))) = (f . ( ~ x)) & ( ~ (f . ( ~ y))) = (f . ( ~ y));

        hence thesis by A1, A7, Th1;

      end;

      thus g is antitone implies f is antitone

      proof

        assume

         A8: for x,y be Element of (S opp ) st x <= y holds for a,b be Element of T st a = (g . x) & b = (g . y) holds a >= b;

        let x,y be Element of S;

        assume x <= y;

        then (y ~ ) <= (x ~ ) by LATTICE3: 9;

        then

         A9: (g . (y ~ )) >= (g . (x ~ )) by A8;

        ((g . (x ~ )) ~ ) = (g . (x ~ )) & ((g . (y ~ )) ~ ) = (g . (y ~ ));

        hence thesis by A1, A9, LATTICE3: 9;

      end;

    end;

    theorem :: YELLOW_7:42



     Th42: for S,T be non empty RelStr holds for f be Function of S, T, g be Function of (S opp ), (T opp ) st f = g holds (f is monotone iff g is monotone) & (f is antitone iff g is antitone)

    proof

      let S,T be non empty RelStr;

      let f be Function of S, T, g be Function of (S ~ ), (T ~ ) such that

       A1: f = g;

      thus f is monotone implies g is monotone

      proof

        assume

         A2: for x,y be Element of S st x <= y holds (f . x) <= (f . y);

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

        assume x <= y;

        then ( ~ y) <= ( ~ x) by Th1;

        then

         A3: (f . ( ~ y)) <= (f . ( ~ x)) by A2;

        ((f . ( ~ x)) ~ ) = (f . ( ~ x)) & ((f . ( ~ y)) ~ ) = (f . ( ~ y));

        hence thesis by A1, A3, LATTICE3: 9;

      end;

      thus g is monotone implies f is monotone

      proof

        assume

         A4: for x,y be Element of (S ~ ) st x <= y holds (g . x) <= (g . y);

        let x,y be Element of S;

        assume x <= y;

        then (y ~ ) <= (x ~ ) by LATTICE3: 9;

        then

         A5: (g . (y ~ )) <= (g . (x ~ )) by A4;

        ( ~ (g . (x ~ ))) = (g . (x ~ )) & ( ~ (g . (y ~ ))) = (g . (y ~ ));

        hence thesis by A1, A5, Th1;

      end;

      thus f is antitone implies g is antitone

      proof

        assume

         A6: for x,y be Element of S st x <= y holds for a,b be Element of T st a = (f . x) & b = (f . y) holds a >= b;

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

        assume x <= y;

        then ( ~ y) <= ( ~ x) by Th1;

        then

         A7: (f . ( ~ y)) >= (f . ( ~ x)) by A6;

        ((f . ( ~ x)) ~ ) = (f . ( ~ x)) & ((f . ( ~ y)) ~ ) = (f . ( ~ y));

        hence thesis by A1, A7, LATTICE3: 9;

      end;

      thus g is antitone implies f is antitone

      proof

        assume

         A8: for x,y be Element of (S opp ) st x <= y holds for a,b be Element of (T opp ) st a = (g . x) & b = (g . y) holds a >= b;

        let x,y be Element of S;

        assume x <= y;

        then (y ~ ) <= (x ~ ) by LATTICE3: 9;

        then

         A9: (g . (y ~ )) >= (g . (x ~ )) by A8;

        ( ~ (g . (x ~ ))) = (g . (x ~ )) & ( ~ (g . (y ~ ))) = (g . (y ~ ));

        hence thesis by A1, A9, Th1;

      end;

    end;

    theorem :: YELLOW_7:43

    for S,T be non empty RelStr, f be set holds (f is Connection of S, T iff f is Connection of (S ~ ), T) & (f is Connection of S, T iff f is Connection of S, (T ~ )) & (f is Connection of S, T iff f is Connection of (S ~ ), (T ~ ))

    proof

      let S,T be non empty RelStr;

       A1:

      now

        let S,S1,T,T1 be RelStr;

        assume

         A2: the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1;

        let a be Connection of S, T;

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

         A3: a = [f, g] by WAYBEL_1:def 9;

        reconsider g as Function of T1, S1 by A2;

        reconsider f as Function of S1, T1 by A2;

        a = [f, g] by A3;

        hence a is Connection of S1, T1;

      end;

      (S ~ ) = RelStr (# the carrier of S, (the InternalRel of S ~ ) #) & (T ~ ) = RelStr (# the carrier of T, (the InternalRel of T ~ ) #);

      hence thesis by A1;

    end;

    theorem :: YELLOW_7:44

    for S,T be non empty Poset holds for f1 be Function of S, T, g1 be Function of T, S holds for f2 be Function of (S ~ ), (T ~ ), g2 be Function of (T ~ ), (S ~ ) st f1 = f2 & g1 = g2 holds [f1, g1] is Galois iff [g2, f2] is Galois

    proof

      let S,T be non empty Poset;

      let f1 be Function of S, T, g1 be Function of T, S;

      let f2 be Function of (S ~ ), (T ~ ), g2 be Function of (T ~ ), (S ~ ) such that

       A1: f1 = f2 and

       A2: g1 = g2;

      hereby

        assume

         A3: [f1, g1] is Galois;

        then f1 is monotone by WAYBEL_1: 8;

        then

         A4: f2 is monotone by A1, Th42;

         A5:

        now

          let s be Element of (S ~ ), t be Element of (T ~ );



           A6: ((f1 . ( ~ s)) ~ ) = (f1 . ( ~ s)) & ((g1 . ( ~ t)) ~ ) = (g1 . ( ~ t));

          ( ~ t) <= (f1 . ( ~ s)) iff (g1 . ( ~ t)) <= ( ~ s) by A3, WAYBEL_1: 8;

          hence (g2 . t) >= s iff t >= (f2 . s) by A1, A2, A6, Th2;

        end;

        g1 is monotone by A3, WAYBEL_1: 8;

        then g2 is monotone by A2, Th42;

        hence [g2, f2] is Galois by A4, A5;

      end;

      assume

       A7: [g2, f2] is Galois;

      then f2 is monotone by WAYBEL_1: 8;

      then

       A8: f1 is monotone by A1, Th42;

       A9:

      now

        let t be Element of T, s be Element of S;



         A10: ( ~ (f2 . (s ~ ))) = (f2 . (s ~ )) & ( ~ (g2 . (t ~ ))) = (g2 . (t ~ ));

        (s ~ ) <= (g2 . (t ~ )) iff (f2 . (s ~ )) <= (t ~ ) by A7, WAYBEL_1: 8;

        hence t <= (f1 . s) iff (g1 . t) <= s by A1, A2, A10, Th2;

      end;

      g2 is monotone by A7, WAYBEL_1: 8;

      then g1 is monotone by A2, Th42;

      hence thesis by A8, A9;

    end;

    theorem :: YELLOW_7:45



     Th45: for J be set, D be non empty set, K be ManySortedSet of J holds for F be DoubleIndexedSet of K, D holds ( doms F) = K

    proof

      let J be set, D be non empty set, K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;



       A1: ( dom ( doms F)) = ( dom F) by FUNCT_6:def 2;



       A2: ( dom F) = J by PARTFUN1:def 2;

       A3:

      now

        let j be object;

        set f = (F . j);

        assume

         A4: j in J;

        then ((J --> D) . j) = D by FUNCOP_1: 7;

        then

         A5: f is Function of (K . j), D by A4, PBOOLE:def 15;

        (( doms F) . j) = ( dom f) by A2, A4, FUNCT_6: 22;

        hence (( doms F) . j) = (K . j) by A5, FUNCT_2:def 1;

      end;

      ( dom K) = J & (F " ( rng F)) = ( dom F) by PARTFUN1:def 2, RELAT_1: 134;

      hence thesis by A2, A1, A3, FUNCT_1: 2;

    end;

    definition

      let J,D be non empty set, K be non-empty ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;

      let j be Element of J;

      let k be Element of (K . j);

      :: original: ..

      redefine

      func F .. (j,k) -> Element of D ;

      coherence

      proof

        ( dom (F . j)) = (K . j) & ( dom F) = J by FUNCT_2:def 1, PARTFUN1:def 2;

        then (F .. (j,k)) = ((F . j) . k) by FUNCT_5: 38;

        hence thesis;

      end;

    end

    theorem :: YELLOW_7:46

    for L be non empty RelStr holds for J be set, K be ManySortedSet of J holds for x be set holds x is DoubleIndexedSet of K, L iff x is DoubleIndexedSet of K, (L opp );

    theorem :: YELLOW_7:47



     Th47: for L be complete LATTICE holds for J be non empty set, K be non-empty ManySortedSet of J holds for F be DoubleIndexedSet of K, L holds ( Sup ( Infs F)) <= ( Inf ( Sups ( Frege F)))

    proof

      let L be complete LATTICE;

      let J be non empty set, K be non-empty ManySortedSet of J;

      let F be DoubleIndexedSet of K, L;

      ( Inf ( Sups ( Frege F))) is_>=_than ( rng ( Infs F))

      proof

        let x be Element of L;

        assume x in ( rng ( Infs F));

        then

        consider a be Element of J such that

         A1: x = ( Inf (F . a)) by WAYBEL_5: 14;



         A2: x = ( inf ( rng (F . a))) by A1, YELLOW_2:def 6;

        x is_<=_than ( rng ( Sups ( Frege F)))

        proof

          reconsider J9 = ( product ( doms F)) as non empty set;

          let y be Element of L;

          reconsider K9 = (J9 --> J) as ManySortedSet of J9;

          reconsider G = ( Frege F) as DoubleIndexedSet of K9, L;

          assume y in ( rng ( Sups ( Frege F)));

          then

          consider f be Element of J9 such that

           A3: y = ( Sup (G . f)) by WAYBEL_5: 14;

          reconsider f as Element of ( product ( doms F));



           A4: ( dom F) = J & ( dom ( Frege F)) = ( product ( doms F)) by PARTFUN1:def 2;

          then (f . a) in ( dom (F . a)) by WAYBEL_5: 9;

          then

          reconsider j = (f . a) as Element of (K . a);



           A5: ((F . a) . j) in ( rng (( Frege F) . f)) by A4, WAYBEL_5: 9;

          j in ( dom (F . a)) by A4, WAYBEL_5: 9;

          then ((F . a) . j) in ( rng (F . a)) by FUNCT_1:def 3;

          then

           A6: x <= ((F . a) . j) by A2, YELLOW_2: 22;

          y = ( sup ( rng (( Frege F) . f))) by A3, YELLOW_2:def 5;

          then ((F . a) . j) <= y by A5, YELLOW_2: 22;

          hence x <= y by A6, ORDERS_2: 3;

        end;

        then x <= ( inf ( rng ( Sups ( Frege F)))) by YELLOW_0: 33;

        hence thesis by YELLOW_2:def 6;

      end;

      then ( sup ( rng ( Infs F))) <= ( Inf ( Sups ( Frege F))) by YELLOW_0: 32;

      hence thesis by YELLOW_2:def 5;

    end;

    theorem :: YELLOW_7:48



     Th48: for L be complete LATTICE holds L is completely-distributive iff for J be non empty set, K be non-empty ManySortedSet of J holds for F be DoubleIndexedSet of K, L holds ( Sup ( Infs F)) = ( Inf ( Sups ( Frege F)))

    proof

      let L be complete LATTICE;

      thus L is completely-distributive implies for J be non empty set, K be non-empty ManySortedSet of J holds for F be DoubleIndexedSet of K, L holds ( Sup ( Infs F)) = ( Inf ( Sups ( Frege F)))

      proof

        assume that L is complete and

         A1: for J be non empty set, K be non-empty ManySortedSet of J holds for F be DoubleIndexedSet of K, L holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)));

        let J be non empty set, K be non-empty ManySortedSet of J;

        let F be DoubleIndexedSet of K, L;



         A2: ( Inf ( Sups ( Frege F))) = ( Sup ( Infs ( Frege ( Frege F)))) by A1;



         A3: ( dom K) = J by PARTFUN1:def 2;



         A4: ( doms ( Frege F)) = (( product ( doms F)) --> J) by Th45;



         A6: ( doms F) = K by Th45;

        ( rng ( Infs ( Frege ( Frege F)))) is_<=_than ( Sup ( Infs F))

        proof

          reconsider J9 = ( product ( doms ( Frege F))) as non empty set;

          let a be Element of L;

          reconsider K9 = (J9 --> ( product ( doms F))) as ManySortedSet of J9;

          reconsider G = ( Frege ( Frege F)) as DoubleIndexedSet of K9, L;

          assume a in ( rng ( Infs ( Frege ( Frege F))));

          then

          consider g be Element of J9 such that

           A8: a = ( Inf (G . g)) by WAYBEL_5: 14;

          reconsider g9 = g as Function;

          deffunc XX( object) = { (f . (g9 . f)) where f be Element of ( product ( doms F)) : (g9 . f) = $1 };



           A9: ( dom (( product ( doms F)) --> J)) = ( product ( doms F));

          now

            defpred P[ object, object] means $2 in ((K . $1) \ XX($1));

            assume

             A10: for j be Element of J holds ((K . j) \ XX(j)) <> {} ;

             A11:

            now

              let j be object;

              assume j in J;

              then

              reconsider i = j as Element of J;

              set k = the Element of ((K . i) \ XX(j));

              ((K . i) \ XX(i)) <> {} by A10;

              then k in ((K . i) \ XX(i));

              hence ex k be object st P[j, k];

            end;

            consider h be Function such that

             A12: ( dom h) = J & for j be object st j in J holds P[j, (h . j)] from CLASSES1:sch 1( A11);

            now

              let j be object;

              assume j in J;

              then (h . j) in ((K . j) \ XX(j)) by A12;

              hence (h . j) in (( doms F) . j) by A6;

            end;

            then

            reconsider h as Element of ( product ( doms F)) by A6, A3, A12, CARD_3: 9;

            (g9 . h) in (( doms ( Frege F)) . h) by A4, A9, CARD_3: 9;

            then

            reconsider j = (g9 . h) as Element of J by A4;

            (h . (g9 . h)) in XX(j) & (h . j) in ((K . j) \ XX(j)) by A12;

            hence contradiction by XBOOLE_0:def 5;

          end;

          then

          consider j be Element of J such that

           A13: ((K . j) \ XX(j)) = {} ;



           A14: ( rng (F . j)) c= ( rng (G . g))

          proof

            let z be object;

            assume z in ( rng (F . j));

            then

            consider u be object such that

             A15: u in ( dom (F . j)) and

             A16: z = ((F . j) . u) by FUNCT_1:def 3;

            reconsider u as Element of (K . j) by A15;

            u in XX(j) by A13, XBOOLE_0:def 5;

            then

            consider f be Element of ( product ( doms F)) such that

             A17: u = (f . (g9 . f)) and

             A18: (g9 . f) = j;



             A: (G . g) = (( Frege F) .. g9) & (( Frege F) . f) = (F .. f) by PRALG_2:def 2;

            consider gg be Function such that

             BB: f = gg & ( dom gg) = ( dom ( doms F)) & for y be object st y in ( dom ( doms F)) holds (gg . y) in (( doms F) . y) by CARD_3:def 5;



             A25: ( dom F) = J by PARTFUN1:def 2;



             BC: ( dom f) = ( dom F) by FUNCT_6:def 2, BB;

            then j in (( dom F) /\ ( dom f)) by A25, BC;

            then j in ( dom (F .. f)) by PRALG_1:def 19;

            then

             WW: ((F .. f) . j) = ((F . j) . (f . j)) by PRALG_1:def 19;



             A27: ( dom ( Frege F)) = ( product ( doms F)) by PARTFUN1:def 2;

            consider gg1 be Function such that

             BB: g = gg1 & ( dom gg1) = ( dom ( doms ( Frege F))) & for y be object st y in ( dom ( doms ( Frege F))) holds (gg1 . y) in (( doms ( Frege F)) . y) by CARD_3:def 5;

            f in ( dom ( Frege F)) by A27;

            then f in ( dom ( doms ( Frege F))) by FUNCT_6:def 2;

            then f in (( dom ( Frege F)) /\ ( dom g9)) by A27, BB, XBOOLE_0:def 4;

            then f in ( dom (( Frege F) .. g9)) by PRALG_1:def 19;

            then ((G . g) . f) = ((F .. f) . j) by A18, PRALG_1:def 19, A;

            then

             A19: ((G . g) . f) = z by A16, A17, A18, WW;

            ( dom (G . g)) = (K9 . g) & (K9 . g) = ( product ( doms F)) by FUNCT_2:def 1;

            hence thesis by A19, FUNCT_1:def 3;

          end;

           ex_inf_of (( rng (G . g)),L) & ex_inf_of (( rng (F . j)),L) by YELLOW_0: 17;

          then ( inf ( rng (G . g))) <= ( inf ( rng (F . j))) by A14, YELLOW_0: 35;

          then a <= ( inf ( rng (F . j))) by A8, YELLOW_2:def 6;

          then

           A20: a <= ( Inf (F . j)) by YELLOW_2:def 6;

          ( Inf (F . j)) in ( rng ( Infs F)) by WAYBEL_5: 14;

          then ( Inf (F . j)) <= ( sup ( rng ( Infs F))) by YELLOW_2: 22;

          then a <= ( sup ( rng ( Infs F))) by A20, ORDERS_2: 3;

          hence thesis by YELLOW_2:def 5;

        end;

        then ( sup ( rng ( Infs ( Frege ( Frege F))))) <= ( Sup ( Infs F)) by YELLOW_0: 32;

        then

         A21: ( Sup ( Infs ( Frege ( Frege F)))) <= ( Sup ( Infs F)) by YELLOW_2:def 5;

        ( Sup ( Infs F)) <= ( Inf ( Sups ( Frege F))) by Th47;

        hence thesis by A2, A21, ORDERS_2: 2;

      end;

      assume

       A22: for J be non empty set, K be non-empty ManySortedSet of J holds for F be DoubleIndexedSet of K, L holds ( Sup ( Infs F)) = ( Inf ( Sups ( Frege F)));

      thus L is complete;

      let J be non empty set, K be non-empty ManySortedSet of J;

      let F be DoubleIndexedSet of K, L;



       A23: ( dom K) = J by PARTFUN1:def 2;



       A24: ( doms ( Frege F)) = (( product ( doms F)) --> J) by Th45;



       A25: ( dom F) = J by PARTFUN1:def 2;



       A26: ( doms F) = K by Th45;



       A27: ( dom ( Frege F)) = ( product ( doms F)) by PARTFUN1:def 2;

      ( rng ( Sups ( Frege ( Frege F)))) is_>=_than ( Inf ( Sups F))

      proof

        reconsider J9 = ( product ( doms ( Frege F))) as non empty set;

        let a be Element of L;

        reconsider K9 = (J9 --> ( product ( doms F))) as ManySortedSet of J9;

        reconsider G = ( Frege ( Frege F)) as DoubleIndexedSet of K9, L;

        assume a in ( rng ( Sups ( Frege ( Frege F))));

        then

        consider g be Element of J9 such that

         A28: a = ( Sup (G . g)) by WAYBEL_5: 14;

        reconsider g9 = g as Function;

        deffunc XX( object) = { (f . (g9 . f)) where f be Element of ( product ( doms F)) : (g9 . f) = $1 };



         A29: ( dom (( product ( doms F)) --> J)) = ( product ( doms F));

        now

          defpred P[ object, object] means $2 in ((K . $1) \ XX($1));

          assume

           A30: for j be Element of J holds ((K . j) \ XX(j)) <> {} ;

           A31:

          now

            let j be object;

            assume j in J;

            then

            reconsider i = j as Element of J;

            set k = the Element of ((K . i) \ XX(j));

            ((K . i) \ XX(i)) <> {} by A30;

            then k in ((K . i) \ XX(i));

            hence ex k be object st P[j, k];

          end;

          consider h be Function such that

           A32: ( dom h) = J & for j be object st j in J holds P[j, (h . j)] from CLASSES1:sch 1( A31);

          now

            let j be object;

            assume j in J;

            then (h . j) in ((K . j) \ XX(j)) by A32;

            hence (h . j) in (( doms F) . j) by A26;

          end;

          then

          reconsider h as Element of ( product ( doms F)) by A26, A23, A32, CARD_3: 9;

          (g9 . h) in (( doms ( Frege F)) . h) by A24, A29, CARD_3: 9;

          then

          reconsider j = (g9 . h) as Element of J by A24;

          (h . (g9 . h)) in XX(j) & (h . j) in ((K . j) \ XX(j)) by A32;

          hence contradiction by XBOOLE_0:def 5;

        end;

        then

        consider j be Element of J such that

         A33: ((K . j) \ XX(j)) = {} ;



         A34: ( rng (F . j)) c= ( rng (G . g))

        proof

          let z be object;

          assume z in ( rng (F . j));

          then

          consider u be object such that

           A35: u in ( dom (F . j)) and

           A36: z = ((F . j) . u) by FUNCT_1:def 3;

          reconsider u as Element of (K . j) by A35;

          u in XX(j) by A33, XBOOLE_0:def 5;

          then

          consider f be Element of ( product ( doms F)) such that

           A37: u = (f . (g9 . f)) and

           A38: (g9 . f) = j;



           a37: (G . g) = (( Frege F) .. g9) & (( Frege F) . f) = (F .. f) by PRALG_2:def 2;

          consider gg be Function such that

           BB: f = gg & ( dom gg) = ( dom ( doms F)) & for y be object st y in ( dom ( doms F)) holds (gg . y) in (( doms F) . y) by CARD_3:def 5;

          ( dom F) = ( dom f) by BB, FUNCT_6:def 2;

          then j in (( dom F) /\ ( dom f)) by A25, XBOOLE_0:def 4;

          then

           Z1: j in ( dom (F .. f)) by PRALG_1:def 19;

          consider gg1 be Function such that

           BB: g = gg1 & ( dom gg1) = ( dom ( doms ( Frege F))) & for y be object st y in ( dom ( doms ( Frege F))) holds (gg1 . y) in (( doms ( Frege F)) . y) by CARD_3:def 5;

          f in ( dom ( Frege F)) by A27;

          then f in ( dom g9) by BB, FUNCT_6:def 2;

          then f in (( dom ( Frege F)) /\ ( dom g9)) by A27, XBOOLE_0:def 4;

          then

           a38: f in ( dom (( Frege F) .. g9)) by PRALG_1:def 19;

          ((G . g) . f) = ((( Frege F) . f) . (g9 . f)) by a37, a38, PRALG_1:def 19;

          then

           A39: ((G . g) . f) = z by Z1, A36, a37, A37, A38, PRALG_1:def 19;

          ( dom (G . g)) = (K9 . g) & (K9 . g) = ( product ( doms F)) by FUNCT_2:def 1;

          hence thesis by A39, FUNCT_1:def 3;

        end;

         ex_sup_of (( rng (G . g)),L) & ex_sup_of (( rng (F . j)),L) by YELLOW_0: 17;

        then ( sup ( rng (G . g))) >= ( sup ( rng (F . j))) by A34, YELLOW_0: 34;

        then a >= ( sup ( rng (F . j))) by A28, YELLOW_2:def 5;

        then

         A40: a >= ( Sup (F . j)) by YELLOW_2:def 5;

        ( Sup (F . j)) in ( rng ( Sups F)) by WAYBEL_5: 14;

        then ( Sup (F . j)) >= ( inf ( rng ( Sups F))) by YELLOW_2: 22;

        then a >= ( inf ( rng ( Sups F))) by A40, ORDERS_2: 3;

        hence thesis by YELLOW_2:def 6;

      end;

      then ( inf ( rng ( Sups ( Frege ( Frege F))))) >= ( Inf ( Sups F)) by YELLOW_0: 33;

      then

       A41: ( Inf ( Sups ( Frege ( Frege F)))) >= ( Inf ( Sups F)) by YELLOW_2:def 6;

      ( Inf ( Sups F)) >= ( Sup ( Infs ( Frege F))) & ( Sup ( Infs ( Frege F))) = ( Inf ( Sups ( Frege ( Frege F)))) by A22, WAYBEL_5: 16;

      hence thesis by A41, ORDERS_2: 2;

    end;

    theorem :: YELLOW_7:49



     Th49: for L be complete antisymmetric non empty RelStr, F be Function holds ( \\/ (F,L)) = ( //\ (F,(L opp ))) & ( //\ (F,L)) = ( \\/ (F,(L opp )))

    proof

      let L be complete antisymmetric non empty RelStr, F be Function;



      thus ( \\/ (F,L)) = ( "\/" (( rng F),L)) by YELLOW_2:def 5

      .= ( "/\" (( rng F),(L opp ))) by YELLOW_0: 17, Th12

      .= ( //\ (F,(L opp ))) by YELLOW_2:def 6;



      thus ( //\ (F,L)) = ( "/\" (( rng F),L)) by YELLOW_2:def 6

      .= ( "\/" (( rng F),(L opp ))) by YELLOW_0: 17, Th13

      .= ( \\/ (F,(L opp ))) by YELLOW_2:def 5;

    end;

    theorem :: YELLOW_7:50



     Th50: for L be complete antisymmetric non empty RelStr holds for F be Function-yielding Function holds ( \// (F,L)) = ( /\\ (F,(L opp ))) & ( /\\ (F,L)) = ( \// (F,(L opp )))

    proof

      let L be complete antisymmetric non empty RelStr;

      let F be Function-yielding Function;

       A1:

      now

        let x be object;

        assume x in ( dom F);

        then (( \// (F,L)) . x) = ( \\/ ((F . x),L)) & (( /\\ (F,(L opp ))) . x) = ( //\ ((F . x),(L opp ))) by WAYBEL_5:def 1, WAYBEL_5:def 2;

        hence (( \// (F,L)) . x) = (( /\\ (F,(L opp ))) . x) by Th49;

      end;

      ( dom ( \// (F,L))) = ( dom F) & ( dom ( /\\ (F,(L opp )))) = ( dom F) by FUNCT_2:def 1;

      hence ( \// (F,L)) = ( /\\ (F,(L opp ))) by A1, FUNCT_1: 2;

       A2:

      now

        let x be object;

        assume x in ( dom F);

        then (( /\\ (F,L)) . x) = ( //\ ((F . x),L)) & (( \// (F,(L opp ))) . x) = ( \\/ ((F . x),(L opp ))) by WAYBEL_5:def 1, WAYBEL_5:def 2;

        hence (( /\\ (F,L)) . x) = (( \// (F,(L opp ))) . x) by Th49;

      end;

      ( dom ( /\\ (F,L))) = ( dom F) & ( dom ( \// (F,(L opp )))) = ( dom F) by FUNCT_2:def 1;

      hence thesis by A2, FUNCT_1: 2;

    end;

    registration

      cluster completely-distributive -> complete for non empty RelStr;

      coherence by WAYBEL_5:def 3;

    end

    registration

      cluster completely-distributive strict for 1 -element Poset;

      existence

      proof

        set R = the 1 -element strict Poset;

        take R;

        thus thesis;

      end;

    end

    theorem :: YELLOW_7:51

    for L be non empty Poset holds L is completely-distributive iff (L opp ) is completely-distributive

    proof

      let L be non empty Poset;

      thus L is completely-distributive implies (L opp ) is completely-distributive

      proof

        assume

         A1: L is completely-distributive;

        hence (L opp ) is complete;

        let J be non empty set, K be non-empty ManySortedSet of J;

        let F be DoubleIndexedSet of K, (L opp );

        reconsider G = F as DoubleIndexedSet of K, L;



        thus ( Inf ( Sups F)) = ( \\/ (( Sups F),L)) by A1, Th49

        .= ( Sup ( Infs G)) by A1, Th50

        .= ( Inf ( Sups ( Frege G))) by A1, Th48

        .= ( //\ (( Infs ( Frege F)),L)) by A1, Th50

        .= ( Sup ( Infs ( Frege F))) by A1, Th49;

      end;

      assume

       A2: (L opp ) is completely-distributive;

      then

       A3: L is complete non empty Poset by Th17;

      thus L is complete by A2, Th17;

      let J be non empty set, K be non-empty ManySortedSet of J;

      let F be DoubleIndexedSet of K, L;

      reconsider G = F as DoubleIndexedSet of K, (L opp );



      thus ( Inf ( Sups F)) = ( \\/ (( Sups F),(L opp ))) by A3, Th49

      .= ( Sup ( Infs G)) by A3, Th50

      .= ( Inf ( Sups ( Frege G))) by A2, Th48

      .= ( //\ (( Infs ( Frege F)),(L opp ))) by A3, Th50

      .= ( Sup ( Infs ( Frege F))) by A3, Th49;

    end;