waybel_1.miz



    begin

    definition

      let L1,L2 be non empty 1-sorted, f be Function of L1, L2;

      :: original: one-to-one

      redefine

      :: WAYBEL_1:def1

      attr f is one-to-one means for x,y be Element of L1 st (f . x) = (f . y) holds x = y;

      compatibility

      proof

        thus f is one-to-one implies for x,y be Element of L1 st (f . x) = (f . y) holds x = y by FUNCT_2: 19;

        assume for x,y be Element of L1 st (f . x) = (f . y) holds x = y;

        then for x,y be object st x in the carrier of L1 & y in the carrier of L1 holds (f . x) = (f . y) implies x = y;

        hence thesis by FUNCT_2: 19;

      end;

    end

    definition

      let L1,L2 be non empty RelStr, f be Function of L1, L2;

      :: original: monotone

      redefine

      :: WAYBEL_1:def2

      attr f is monotone means for x,y be Element of L1 st x <= y holds (f . x) <= (f . y);

      compatibility ;

    end

    theorem :: WAYBEL_1:1

    

     Th1: for L be antisymmetric transitive with_infima RelStr, x,y,z be Element of L st x <= y holds (x "/\" z) <= (y "/\" z)

    proof

      let L be antisymmetric transitive with_infima RelStr;

      let x,y,z be Element of L;

      

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

      

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

      assume x <= y;

      then (x "/\" z) <= y by A1, ORDERS_2: 3;

      hence thesis by A2, YELLOW_0: 23;

    end;

    theorem :: WAYBEL_1:2

    

     Th2: for L be antisymmetric transitive with_suprema RelStr, x,y,z be Element of L st x <= y holds (x "\/" z) <= (y "\/" z)

    proof

      let L be antisymmetric transitive with_suprema RelStr;

      let x,y,z be Element of L;

      

       A1: y <= (y "\/" z) by YELLOW_0: 22;

      

       A2: z <= (y "\/" z) by YELLOW_0: 22;

      assume x <= y;

      then x <= (y "\/" z) by A1, ORDERS_2: 3;

      hence thesis by A2, YELLOW_0: 22;

    end;

    theorem :: WAYBEL_1:3

    

     Th3: for L be non empty lower-bounded antisymmetric RelStr holds for x be Element of L holds (L is with_infima implies (( Bottom L) "/\" x) = ( Bottom L)) & (L is with_suprema reflexive transitive implies (( Bottom L) "\/" x) = x)

    proof

      let L be non empty lower-bounded antisymmetric RelStr;

      let x be Element of L;

      thus L is with_infima implies (( Bottom L) "/\" x) = ( Bottom L)

      proof

        assume L is with_infima;

        then ( Bottom L) <= (( Bottom L) "/\" x) & (( Bottom L) "/\" x) <= ( Bottom L) by YELLOW_0: 23, YELLOW_0: 44;

        hence thesis by ORDERS_2: 2;

      end;

      assume

       A1: L is with_suprema;

      then

       A2: x <= (( Bottom L) "\/" x) by YELLOW_0: 22;

      assume L is reflexive transitive;

      then

       A3: x <= x;

      ( Bottom L) <= x by YELLOW_0: 44;

      then (( Bottom L) "\/" x) <= x by A1, A3, YELLOW_0: 22;

      hence thesis by A2, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_1:4

    

     Th4: for L be non empty upper-bounded antisymmetric RelStr holds for x be Element of L holds (L is with_infima transitive reflexive implies (( Top L) "/\" x) = x) & (L is with_suprema implies (( Top L) "\/" x) = ( Top L))

    proof

      let L be non empty upper-bounded antisymmetric RelStr, x be Element of L;

      thus L is with_infima transitive reflexive implies (( Top L) "/\" x) = x

      proof

        assume

         A1: L is with_infima transitive reflexive;

        then (x "/\" x) <= (( Top L) "/\" x) by Th1, YELLOW_0: 45;

        then

         A2: x <= (( Top L) "/\" x) by A1, YELLOW_0: 25;

        (( Top L) "/\" x) <= x by A1, YELLOW_0: 23;

        hence thesis by A2, ORDERS_2: 2;

      end;

      assume L is with_suprema;

      then (( Top L) "\/" x) <= ( Top L) & ( Top L) <= (( Top L) "\/" x) by YELLOW_0: 22, YELLOW_0: 45;

      hence thesis by ORDERS_2: 2;

    end;

    definition

      let L be non empty RelStr;

      :: WAYBEL_1:def3

      attr L is distributive means

      : Def3: for x,y,z be Element of L holds (x "/\" (y "\/" z)) = ((x "/\" y) "\/" (x "/\" z));

    end

    theorem :: WAYBEL_1:5

    

     Th5: for L be LATTICE holds L is distributive iff for x,y,z be Element of L holds (x "\/" (y "/\" z)) = ((x "\/" y) "/\" (x "\/" z))

    proof

      let L be LATTICE;

      hereby

        assume

         A1: L is distributive;

        let x,y,z be Element of L;

        

        thus (x "\/" (y "/\" z)) = ((x "\/" (z "/\" x)) "\/" (y "/\" z)) by LATTICE3: 17

        .= (x "\/" ((z "/\" x) "\/" (z "/\" y))) by LATTICE3: 14

        .= (x "\/" ((x "\/" y) "/\" z)) by A1

        .= (((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" z)) by LATTICE3: 18

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

      end;

      assume

       A2: for x,y,z be Element of L holds (x "\/" (y "/\" z)) = ((x "\/" y) "/\" (x "\/" z));

      let x,y,z be Element of L;

      

      thus (x "/\" (y "\/" z)) = ((x "/\" (x "\/" z)) "/\" (y "\/" z)) by LATTICE3: 18

      .= (x "/\" ((z "\/" x) "/\" (y "\/" z))) by LATTICE3: 16

      .= (x "/\" (z "\/" (x "/\" y))) by A2

      .= (((y "/\" x) "\/" x) "/\" ((x "/\" y) "\/" z)) by LATTICE3: 17

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

    end;

    registration

      let X be set;

      cluster ( BoolePoset X) -> distributive;

      coherence

      proof

        let x,y,z be Element of ( BoolePoset X);

        

        thus (x "/\" (y "\/" z)) = (x /\ (y "\/" z)) by YELLOW_1: 17

        .= (x /\ (y \/ z)) by YELLOW_1: 17

        .= ((x /\ y) \/ (x /\ z)) by XBOOLE_1: 23

        .= ((x "/\" y) \/ (x /\ z)) by YELLOW_1: 17

        .= ((x "/\" y) \/ (x "/\" z)) by YELLOW_1: 17

        .= ((x "/\" y) "\/" (x "/\" z)) by YELLOW_1: 17;

      end;

    end

    definition

      let S be non empty RelStr, X be set;

      :: WAYBEL_1:def4

      pred ex_min_of X,S means ex_inf_of (X,S) & ( "/\" (X,S)) in X;

      :: WAYBEL_1:def5

      pred ex_max_of X,S means ex_sup_of (X,S) & ( "\/" (X,S)) in X;

    end

    notation

      let S be non empty RelStr, X be set;

      synonym X has_the_min_in S for ex_min_of X,S;

      synonym X has_the_max_in S for ex_max_of X,S;

    end

    definition

      let S be non empty RelStr, s be Element of S, X be set;

      :: WAYBEL_1:def6

      pred s is_minimum_of X means ex_inf_of (X,S) & s = ( "/\" (X,S)) & ( "/\" (X,S)) in X;

      :: WAYBEL_1:def7

      pred s is_maximum_of X means ex_sup_of (X,S) & s = ( "\/" (X,S)) & ( "\/" (X,S)) in X;

    end

    registration

      let L be RelStr;

      cluster ( id L) -> isomorphic;

      coherence

      proof

        per cases ;

          suppose

           A1: L is non empty;

          

           A2: ( id L) = (( id L) " ) by FUNCT_1: 45;

          ( id L) is monotone;

          hence thesis by A1, A2, WAYBEL_0:def 38;

        end;

          suppose L is empty;

          hence thesis by WAYBEL_0:def 38;

        end;

      end;

    end

    definition

      let L1,L2 be RelStr;

      :: WAYBEL_1:def8

      pred L1,L2 are_isomorphic means ex f be Function of L1, L2 st f is isomorphic;

      reflexivity

      proof

        let L be RelStr;

        take ( id L);

        thus thesis;

      end;

    end

    theorem :: WAYBEL_1:6

    for L1,L2 be non empty RelStr st (L1,L2) are_isomorphic holds (L2,L1) are_isomorphic

    proof

      let L1,L2 be non empty RelStr;

      given f be Function of L1, L2 such that

       A1: f is isomorphic;

      consider g be Function of L2, L1 such that

       A2: g = (f qua Function " ) and

       A3: g is monotone by A1, WAYBEL_0:def 38;

      f = (g qua Function " ) by A1, A2, FUNCT_1: 43;

      then g is isomorphic by A1, A2, A3, WAYBEL_0:def 38;

      hence thesis;

    end;

    theorem :: WAYBEL_1:7

    for L1,L2,L3 be RelStr st (L1,L2) are_isomorphic & (L2,L3) are_isomorphic holds (L1,L3) are_isomorphic

    proof

      let L1,L2,L3 be RelStr;

      given f1 be Function of L1, L2 such that

       A1: f1 is isomorphic;

      given f2 be Function of L2, L3 such that

       A2: f2 is isomorphic;

      

       A3: L1 is empty implies (f2 * f1) is Function of L1, L3 by FUNCT_2: 13;

      per cases ;

        suppose L1 is non empty & L2 is non empty & L3 is non empty;

        then

        reconsider L1, L2, L3 as non empty RelStr;

        reconsider f1 as Function of L1, L2;

        reconsider f2 as Function of L2, L3;

        consider g1 be Function of L2, L1 such that

         A4: g1 = (f1 qua Function " ) & g1 is monotone by A1, WAYBEL_0:def 38;

        consider g2 be Function of L3, L2 such that

         A5: g2 = (f2 qua Function " ) & g2 is monotone by A2, WAYBEL_0:def 38;

        

         A6: (f2 * f1) is monotone by A1, A2, YELLOW_2: 12;

        (g1 * g2) is monotone & (g1 * g2) = ((f2 * f1) qua Function " ) by A1, A2, A4, A5, FUNCT_1: 44, YELLOW_2: 12;

        then (f2 * f1) is isomorphic by A1, A2, A6, WAYBEL_0:def 38;

        hence thesis;

      end;

        suppose

         A7: L1 is empty;

        then

        reconsider f = (f2 * f1) as Function of L1, L3 by A3;

        L2 is empty by A1, A7, WAYBEL_0:def 38;

        then L3 is empty by A2, WAYBEL_0:def 38;

        then f is isomorphic by A7, WAYBEL_0:def 38;

        hence thesis;

      end;

        suppose

         A8: L2 is empty;

        then

        reconsider f = (f2 * f1) as Function of L1, L3 by A1, A3, WAYBEL_0:def 38;

        L1 is empty & L3 is empty by A1, A2, A8, WAYBEL_0:def 38;

        then f is isomorphic by WAYBEL_0:def 38;

        hence thesis;

      end;

        suppose

         A9: L3 is empty;

        then

         A10: L2 is empty by A2, WAYBEL_0:def 38;

        then

        reconsider f = (f2 * f1) as Function of L1, L3 by A1, A3, WAYBEL_0:def 38;

        L1 is empty by A1, A10, WAYBEL_0:def 38;

        then f is isomorphic by A9, WAYBEL_0:def 38;

        hence thesis;

      end;

    end;

    begin

    definition

      let S,T be RelStr;

      :: WAYBEL_1:def9

      mode Connection of S,T -> set means

      : Def9: ex g be Function of S, T, d be Function of T, S st it = [g, d];

      existence

      proof

        set g = the Function of S, T, d = the Function of T, S;

        take [g, d];

        thus thesis;

      end;

    end

    definition

      let S,T be RelStr, g be Function of S, T, d be Function of T, S;

      :: original: [

      redefine

      func [g,d] -> Connection of S, T ;

      coherence by Def9;

    end

    definition

      let S,T be non empty RelStr, gc be Connection of S, T;

      :: WAYBEL_1:def10

      attr gc is Galois means ex g be Function of S, T, d be Function of T, S st gc = [g, d] & g is monotone & d is monotone & for t be Element of T, s be Element of S holds t <= (g . s) iff (d . t) <= s;

    end

    theorem :: WAYBEL_1:8

    

     Th8: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S holds [g, d] is Galois iff g is monotone & d is monotone & for t be Element of T, s be Element of S holds t <= (g . s) iff (d . t) <= s

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      hereby

        assume [g, d] is Galois;

        then

        consider g9 be Function of S, T, d9 be Function of T, S such that

         A1: [g, d] = [g9, d9] and

         A2: g9 is monotone & d9 is monotone & for t be Element of T, s be Element of S holds t <= (g9 . s) iff (d9 . t) <= s;

        g = g9 & d = d9 by A1, XTUPLE_0: 1;

        hence g is monotone & d is monotone & for t be Element of T, s be Element of S holds t <= (g . s) iff (d . t) <= s by A2;

      end;

      thus thesis;

    end;

    definition

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

      :: WAYBEL_1:def11

      attr g is upper_adjoint means ex d be Function of T, S st [g, d] is Galois;

    end

    definition

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

      :: WAYBEL_1:def12

      attr d is lower_adjoint means

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

    end

    theorem :: WAYBEL_1:9

    for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st [g, d] is Galois holds g is upper_adjoint & d is lower_adjoint;

    theorem :: WAYBEL_1:10

    

     Th10: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S holds [g, d] is Galois iff g is monotone & for t be Element of T holds (d . t) is_minimum_of (g " ( uparrow t))

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      hereby

        assume

         A1: [g, d] is Galois;

        hence g is monotone by Th8;

        let t be Element of T;

        thus (d . t) is_minimum_of (g " ( uparrow t))

        proof

          set X = (g " ( uparrow t));

          t <= (g . (d . t)) by A1, Th8;

          then (g . (d . t)) in ( uparrow t) by WAYBEL_0: 18;

          then

           A2: (d . t) in X by FUNCT_2: 38;

          then

           A3: for s be Element of S st s is_<=_than X holds (d . t) >= s;

          

           A4: (d . t) is_<=_than X

          proof

            let s be Element of S;

            assume s in X;

            then (g . s) in ( uparrow t) by FUNCT_1:def 7;

            then t <= (g . s) by WAYBEL_0: 18;

            hence (d . t) <= s by A1, Th8;

          end;

          hence ex_inf_of (X,S) & (d . t) = ( inf X) by A3, YELLOW_0: 31;

          thus thesis by A4, A2, A3, YELLOW_0: 31;

        end;

      end;

      assume that

       A5: g is monotone and

       A6: for t be Element of T holds (d . t) is_minimum_of (g " ( uparrow t));

      

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

      proof

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

        set X = (g " ( uparrow t));

        hereby

          assume t <= (g . s);

          then (g . s) in ( uparrow t) by WAYBEL_0: 18;

          then

           A8: s in X by FUNCT_2: 38;

          

           A9: (d . t) is_minimum_of (g " ( uparrow t)) by A6;

          then ex_inf_of (X,S);

          then X is_>=_than ( inf X) by YELLOW_0:def 10;

          then s >= ( inf X) by A8;

          hence (d . t) <= s by A9;

        end;

        

         A10: (d . t) is_minimum_of X by A6;

        then ( inf X) in X;

        then (g . ( inf X)) in ( uparrow t) by FUNCT_1:def 7;

        then (g . ( inf X)) >= t by WAYBEL_0: 18;

        then

         A11: (g . (d . t)) >= t by A10;

        assume (d . t) <= s;

        then (g . (d . t)) <= (g . s) by A5;

        hence thesis by A11, ORDERS_2: 3;

      end;

      d is monotone

      proof

        let t1,t2 be Element of T;

        assume t1 <= t2;

        then

         A12: ( uparrow t2) c= ( uparrow t1) by WAYBEL_0: 22;

        

         A13: (d . t2) is_minimum_of (g " ( uparrow t2)) by A6;

        then

         A14: ex_inf_of ((g " ( uparrow t2)),S);

        

         A15: (d . t1) is_minimum_of (g " ( uparrow t1)) by A6;

        then ex_inf_of ((g " ( uparrow t1)),S);

        then ( inf (g " ( uparrow t1))) <= ( inf (g " ( uparrow t2))) by A14, A12, RELAT_1: 143, YELLOW_0: 35;

        then (d . t1) <= ( inf (g " ( uparrow t2))) by A15;

        hence (d . t1) <= (d . t2) by A13;

      end;

      hence thesis by A5, A7;

    end;

    theorem :: WAYBEL_1:11

    

     Th11: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S holds [g, d] is Galois iff d is monotone & for s be Element of S holds (g . s) is_maximum_of (d " ( downarrow s))

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      hereby

        assume

         A1: [g, d] is Galois;

        hence d is monotone by Th8;

        let s be Element of S;

        thus (g . s) is_maximum_of (d " ( downarrow s))

        proof

          set X = (d " ( downarrow s));

          s >= (d . (g . s)) by A1, Th8;

          then (d . (g . s)) in ( downarrow s) by WAYBEL_0: 17;

          then

           A2: (g . s) in X by FUNCT_2: 38;

          then

           A3: for t be Element of T st t is_>=_than X holds (g . s) <= t;

          

           A4: (g . s) is_>=_than X

          proof

            let t be Element of T;

            assume t in X;

            then (d . t) in ( downarrow s) by FUNCT_1:def 7;

            then s >= (d . t) by WAYBEL_0: 17;

            hence thesis by A1, Th8;

          end;

          hence ex_sup_of (X,T) & (g . s) = ( sup X) by A3, YELLOW_0: 30;

          thus thesis by A4, A2, A3, YELLOW_0: 30;

        end;

      end;

      assume that

       A5: d is monotone and

       A6: for s be Element of S holds (g . s) is_maximum_of (d " ( downarrow s));

      

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

      proof

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

        set X = (d " ( downarrow s));

        

         A8: (g . s) is_maximum_of X by A6;

        then ( sup X) in X;

        then (d . ( sup X)) in ( downarrow s) by FUNCT_1:def 7;

        then (d . ( sup X)) <= s by WAYBEL_0: 17;

        then

         A9: (d . (g . s)) <= s by A8;

        hereby

          assume s >= (d . t);

          then (d . t) in ( downarrow s) by WAYBEL_0: 17;

          then

           A10: t in X by FUNCT_2: 38;

           ex_sup_of (X,T) by A8;

          then X is_<=_than ( sup X) by YELLOW_0:def 9;

          then t <= ( sup X) by A10;

          hence (g . s) >= t by A8;

        end;

        assume (g . s) >= t;

        then (d . (g . s)) >= (d . t) by A5;

        hence thesis by A9, ORDERS_2: 3;

      end;

      g is monotone

      proof

        let s1,s2 be Element of S;

        assume s1 <= s2;

        then

         A11: ( downarrow s1) c= ( downarrow s2) by WAYBEL_0: 21;

        

         A12: (g . s2) is_maximum_of (d " ( downarrow s2)) by A6;

        then

         A13: ex_sup_of ((d " ( downarrow s2)),T);

        

         A14: (g . s1) is_maximum_of (d " ( downarrow s1)) by A6;

        then ex_sup_of ((d " ( downarrow s1)),T);

        then ( sup (d " ( downarrow s1))) <= ( sup (d " ( downarrow s2))) by A13, A11, RELAT_1: 143, YELLOW_0: 34;

        then (g . s1) <= ( sup (d " ( downarrow s2))) by A14;

        hence (g . s1) <= (g . s2) by A12;

      end;

      hence thesis by A5, A7;

    end;

    theorem :: WAYBEL_1:12

    

     Th12: for S,T be non empty Poset, g be Function of S, T st g is upper_adjoint holds g is infs-preserving

    proof

      let S,T be non empty Poset, g be Function of S, T;

      given d be Function of T, S such that

       A1: [g, d] is Galois;

      let X be Subset of S;

      set s = ( inf X);

      assume

       A2: ex_inf_of (X,S);

      

       A3: for t be Element of T st t is_<=_than (g .: X) holds (g . s) >= t

      proof

        let t be Element of T;

        assume

         A4: t is_<=_than (g .: X);

        (d . t) is_<=_than X

        proof

          let si be Element of S;

          assume si in X;

          then (g . si) in (g .: X) by FUNCT_2: 35;

          then t <= (g . si) by A4;

          hence (d . t) <= si by A1, Th8;

        end;

        then (d . t) <= s by A2, YELLOW_0: 31;

        hence thesis by A1, Th8;

      end;

      (g . s) is_<=_than (g .: X)

      proof

        let t be Element of T;

        assume t in (g .: X);

        then

        consider si be Element of S such that

         A5: si in X and

         A6: t = (g . si) by FUNCT_2: 65;

        

         A7: g is monotone by A1, Th8;

        reconsider si as Element of S;

        s is_<=_than X by A2, YELLOW_0: 31;

        then s <= si by A5;

        hence (g . s) <= t by A7, A6;

      end;

      hence thesis by A3, YELLOW_0: 31;

    end;

    registration

      let S,T be non empty Poset;

      cluster upper_adjoint -> infs-preserving for Function of S, T;

      coherence by Th12;

    end

    theorem :: WAYBEL_1:13

    

     Th13: for S,T be non empty Poset, d be Function of T, S st d is lower_adjoint holds d is sups-preserving

    proof

      let S,T be non empty Poset, d be Function of T, S;

      given g be Function of S, T such that

       A1: [g, d] is Galois;

      let X be Subset of T;

      set t = ( sup X);

      assume

       A2: ex_sup_of (X,T);

      

       A3: for s be Element of S st s is_>=_than (d .: X) holds (d . t) <= s

      proof

        let s be Element of S;

        assume

         A4: s is_>=_than (d .: X);

        (g . s) is_>=_than X

        proof

          let ti be Element of T;

          assume ti in X;

          then (d . ti) in (d .: X) by FUNCT_2: 35;

          then s >= (d . ti) by A4;

          hence thesis by A1, Th8;

        end;

        then (g . s) >= t by A2, YELLOW_0: 30;

        hence thesis by A1, Th8;

      end;

      (d . t) is_>=_than (d .: X)

      proof

        let s be Element of S;

        assume s in (d .: X);

        then

        consider ti be Element of T such that

         A5: ti in X and

         A6: s = (d . ti) by FUNCT_2: 65;

        

         A7: d is monotone by A1, Th8;

        reconsider ti as Element of T;

        t is_>=_than X by A2, YELLOW_0: 30;

        then t >= ti by A5;

        hence thesis by A7, A6;

      end;

      hence thesis by A3, YELLOW_0: 30;

    end;

    registration

      let S,T be non empty Poset;

      cluster lower_adjoint -> sups-preserving for Function of S, T;

      coherence by Th13;

    end

    theorem :: WAYBEL_1:14

    

     Th14: for S,T be non empty Poset, g be Function of S, T st S is complete & g is infs-preserving holds ex d be Function of T, S st [g, d] is Galois & for t be Element of T holds (d . t) is_minimum_of (g " ( uparrow t))

    proof

      let S,T be non empty Poset, g be Function of S, T;

      assume that

       A1: S is complete and

       A2: g is infs-preserving;

      defpred P[ object, object] means ex t be Element of T st t = $1 & $2 = ( inf (g " ( uparrow t)));

      

       A3: for e be object st e in the carrier of T holds ex u be object st u in the carrier of S & P[e, u]

      proof

        let e be object;

        assume e in the carrier of T;

        then

        reconsider t = e as Element of T;

        take ( inf (g " ( uparrow t)));

        thus thesis;

      end;

      consider d be Function of the carrier of T, the carrier of S such that

       A4: for e be object st e in the carrier of T holds P[e, (d . e)] from FUNCT_2:sch 1( A3);

      

       A5: for t be Element of T holds (d . t) = ( inf (g " ( uparrow t)))

      proof

        let t be Element of T;

        ex t1 be Element of T st t1 = t & (d . t) = ( inf (g " ( uparrow t1))) by A4;

        hence thesis;

      end;

      reconsider d as Function of T, S;

      for X be Filter of S holds g preserves_inf_of X by A2;

      then

       A6: g is monotone by WAYBEL_0: 69;

      

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

      proof

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

        

         A8: ex_inf_of (( uparrow t),T) by WAYBEL_0: 39;

        

         A9: ex_inf_of ((g " ( uparrow t)),S) by A1, YELLOW_0: 17;

        then ( inf (g " ( uparrow t))) is_<=_than (g " ( uparrow t)) by YELLOW_0: 31;

        then

         A10: (d . t) is_<=_than (g " ( uparrow t)) by A5;

        hereby

          assume t <= (g . s);

          then (g . s) in ( uparrow t) by WAYBEL_0: 18;

          then s in (g " ( uparrow t)) by FUNCT_2: 38;

          hence (d . t) <= s by A10;

        end;

        g preserves_inf_of (g " ( uparrow t)) by A2;

        then ex_inf_of ((g .: (g " ( uparrow t))),T) & (g . ( inf (g " ( uparrow t)))) = ( inf (g .: (g " ( uparrow t)))) by A9;

        then (g . ( inf (g " ( uparrow t)))) >= ( inf ( uparrow t)) by A8, FUNCT_1: 75, YELLOW_0: 35;

        then

         A11: (g . ( inf (g " ( uparrow t)))) >= t by WAYBEL_0: 39;

        assume (d . t) <= s;

        then (g . (d . t)) <= (g . s) by A6;

        then (g . ( inf (g " ( uparrow t)))) <= (g . s) by A5;

        hence thesis by A11, ORDERS_2: 3;

      end;

      take d;

      d is monotone

      proof

        let t1,t2 be Element of T;

        assume t1 <= t2;

        then

         A12: ( uparrow t2) c= ( uparrow t1) by WAYBEL_0: 22;

         ex_inf_of ((g " ( uparrow t1)),S) & ex_inf_of ((g " ( uparrow t2)),S) by A1, YELLOW_0: 17;

        then ( inf (g " ( uparrow t1))) <= ( inf (g " ( uparrow t2))) by A12, RELAT_1: 143, YELLOW_0: 35;

        then (d . t1) <= ( inf (g " ( uparrow t2))) by A5;

        hence (d . t1) <= (d . t2) by A5;

      end;

      hence [g, d] is Galois by A6, A7;

      let t be Element of T;

      thus

       A13: ex_inf_of ((g " ( uparrow t)),S) by A1, YELLOW_0: 17;

      thus

       A14: (d . t) = ( inf (g " ( uparrow t))) by A5;

      

       A15: ex_inf_of (( uparrow t),T) by WAYBEL_0: 39;

      g preserves_inf_of (g " ( uparrow t)) by A2;

      then ex_inf_of ((g .: (g " ( uparrow t))),T) & (g . ( inf (g " ( uparrow t)))) = ( inf (g .: (g " ( uparrow t)))) by A13;

      then (g . ( inf (g " ( uparrow t)))) >= ( inf ( uparrow t)) by A15, FUNCT_1: 75, YELLOW_0: 35;

      then (g . ( inf (g " ( uparrow t)))) >= t by WAYBEL_0: 39;

      then (g . (d . t)) >= t by A5;

      then (g . (d . t)) in ( uparrow t) by WAYBEL_0: 18;

      hence thesis by A14, FUNCT_2: 38;

    end;

    theorem :: WAYBEL_1:15

    

     Th15: for S,T be non empty Poset, d be Function of T, S st T is complete & d is sups-preserving holds ex g be Function of S, T st [g, d] is Galois & for s be Element of S holds (g . s) is_maximum_of (d " ( downarrow s))

    proof

      let S,T be non empty Poset, d be Function of T, S;

      assume that

       A1: T is complete and

       A2: d is sups-preserving;

      defpred P[ object, object] means ex s be Element of S st s = $1 & $2 = ( sup (d " ( downarrow s)));

      

       A3: for e be object st e in the carrier of S holds ex u be object st u in the carrier of T & P[e, u]

      proof

        let e be object;

        assume e in the carrier of S;

        then

        reconsider s = e as Element of S;

        take ( sup (d " ( downarrow s)));

        thus thesis;

      end;

      consider g be Function of the carrier of S, the carrier of T such that

       A4: for e be object st e in the carrier of S holds P[e, (g . e)] from FUNCT_2:sch 1( A3);

      

       A5: for s be Element of S holds (g . s) = ( sup (d " ( downarrow s)))

      proof

        let s be Element of S;

        ex s1 be Element of S st s1 = s & (g . s) = ( sup (d " ( downarrow s1))) by A4;

        hence thesis;

      end;

      reconsider g as Function of S, T;

      for X be Ideal of T holds d preserves_sup_of X by A2;

      then

       A6: d is monotone by WAYBEL_0: 72;

      

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

      proof

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

        

         A8: ex_sup_of (( downarrow s),S) by WAYBEL_0: 34;

        

         A9: ex_sup_of ((d " ( downarrow s)),T) by A1, YELLOW_0: 17;

        then ( sup (d " ( downarrow s))) is_>=_than (d " ( downarrow s)) by YELLOW_0: 30;

        then

         A10: (g . s) is_>=_than (d " ( downarrow s)) by A5;

        hereby

          assume s >= (d . t);

          then (d . t) in ( downarrow s) by WAYBEL_0: 17;

          then t in (d " ( downarrow s)) by FUNCT_2: 38;

          hence (g . s) >= t by A10;

        end;

        d preserves_sup_of (d " ( downarrow s)) by A2;

        then ex_sup_of ((d .: (d " ( downarrow s))),S) & (d . ( sup (d " ( downarrow s)))) = ( sup (d .: (d " ( downarrow s)))) by A9;

        then (d . ( sup (d " ( downarrow s)))) <= ( sup ( downarrow s)) by A8, FUNCT_1: 75, YELLOW_0: 34;

        then

         A11: (d . ( sup (d " ( downarrow s)))) <= s by WAYBEL_0: 34;

        assume (g . s) >= t;

        then (d . (g . s)) >= (d . t) by A6;

        then (d . ( sup (d " ( downarrow s)))) >= (d . t) by A5;

        hence thesis by A11, ORDERS_2: 3;

      end;

      take g;

      g is monotone

      proof

        let s1,s2 be Element of S;

        assume s1 <= s2;

        then

         A12: ( downarrow s1) c= ( downarrow s2) by WAYBEL_0: 21;

         ex_sup_of ((d " ( downarrow s1)),T) & ex_sup_of ((d " ( downarrow s2)),T) by A1, YELLOW_0: 17;

        then ( sup (d " ( downarrow s1))) <= ( sup (d " ( downarrow s2))) by A12, RELAT_1: 143, YELLOW_0: 34;

        then (g . s1) <= ( sup (d " ( downarrow s2))) by A5;

        hence (g . s1) <= (g . s2) by A5;

      end;

      hence [g, d] is Galois by A6, A7;

      let s be Element of S;

      thus

       A13: ex_sup_of ((d " ( downarrow s)),T) by A1, YELLOW_0: 17;

      thus

       A14: (g . s) = ( sup (d " ( downarrow s))) by A5;

      

       A15: ex_sup_of (( downarrow s),S) by WAYBEL_0: 34;

      d preserves_sup_of (d " ( downarrow s)) by A2;

      then ex_sup_of ((d .: (d " ( downarrow s))),S) & (d . ( sup (d " ( downarrow s)))) = ( sup (d .: (d " ( downarrow s)))) by A13;

      then (d . ( sup (d " ( downarrow s)))) <= ( sup ( downarrow s)) by A15, FUNCT_1: 75, YELLOW_0: 34;

      then (d . ( sup (d " ( downarrow s)))) <= s by WAYBEL_0: 34;

      then (d . (g . s)) <= s by A5;

      then (d . (g . s)) in ( downarrow s) by WAYBEL_0: 17;

      hence thesis by A14, FUNCT_2: 38;

    end;

    theorem :: WAYBEL_1:16

    for S,T be non empty Poset, g be Function of S, T st S is complete holds (g is infs-preserving iff g is monotone & g is upper_adjoint)

    proof

      let S,T be non empty Poset, g be Function of S, T;

      assume

       A1: S is complete;

      hereby

        assume g is infs-preserving;

        then ex d be Function of T, S st [g, d] is Galois & for t be Element of T holds (d . t) is_minimum_of (g " ( uparrow t)) by A1, Th14;

        hence g is monotone & g is upper_adjoint by Th10;

      end;

      assume g is monotone;

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

      then g is upper_adjoint;

      hence thesis;

    end;

    theorem :: WAYBEL_1:17

    

     Th17: for S,T be non empty Poset, d be Function of T, S st T is complete holds d is sups-preserving iff d is monotone & d is lower_adjoint

    proof

      let S,T be non empty Poset, d be Function of T, S;

      assume

       A1: T is complete;

      hereby

        assume d is sups-preserving;

        then ex g be Function of S, T st [g, d] is Galois & for s be Element of S holds (g . s) is_maximum_of (d " ( downarrow s)) by A1, Th15;

        hence d is monotone & d is lower_adjoint by Th11;

      end;

      assume d is monotone;

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

      then d is lower_adjoint;

      hence thesis;

    end;

    theorem :: WAYBEL_1:18

    

     Th18: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st [g, d] is Galois holds (d * g) <= ( id S) & ( id T) <= (g * d)

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      assume

       A1: [g, d] is Galois;

      for s be Element of S holds ((d * g) . s) <= (( id S) . s)

      proof

        let s be Element of S;

        (d . (g . s)) <= s by A1, Th8;

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

        hence thesis;

      end;

      hence (d * g) <= ( id S) by YELLOW_2: 9;

      for t be Element of T holds (( id T) . t) <= ((g * d) . t)

      proof

        let t be Element of T;

        t <= (g . (d . t)) by A1, Th8;

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

        hence thesis;

      end;

      hence thesis by YELLOW_2: 9;

    end;

    theorem :: WAYBEL_1:19

    

     Th19: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st g is monotone & d is monotone & (d * g) <= ( id S) & ( id T) <= (g * d) holds [g, d] is Galois

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      assume that

       A1: g is monotone and

       A2: d is monotone and

       A3: (d * g) <= ( id S) and

       A4: ( id T) <= (g * d);

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

      proof

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

        hereby

          ((d * g) . s) <= (( id S) . s) by A3, YELLOW_2: 9;

          then (d . (g . s)) <= (( id S) . s) by FUNCT_2: 15;

          then

           A5: (d . (g . s)) <= s;

          assume t <= (g . s);

          then (d . t) <= (d . (g . s)) by A2;

          hence (d . t) <= s by A5, ORDERS_2: 3;

        end;

        (( id T) . t) <= ((g * d) . t) by A4, YELLOW_2: 9;

        then (( id T) . t) <= (g . (d . t)) by FUNCT_2: 15;

        then

         A6: t <= (g . (d . t));

        assume (d . t) <= s;

        then (g . (d . t)) <= (g . s) by A1;

        hence thesis by A6, ORDERS_2: 3;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: WAYBEL_1:20

    

     Th20: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st g is monotone & d is monotone & (d * g) <= ( id S) & ( id T) <= (g * d) holds d = ((d * g) * d) & g = ((g * d) * g)

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      assume that

       A1: g is monotone and

       A2: d is monotone and

       A3: (d * g) <= ( id S) and

       A4: ( id T) <= (g * d);

      for t be Element of T holds (d . t) = (((d * g) * d) . t)

      proof

        let t be Element of T;

        (( id T) . t) <= ((g * d) . t) by A4, YELLOW_2: 9;

        then t <= ((g * d) . t);

        then (d . t) <= (d . ((g * d) . t)) by A2;

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

        then

         A5: (d . t) <= (((d * g) * d) . t) by RELAT_1: 36;

        ((d * g) . (d . t)) <= (( id S) . (d . t)) by A3, YELLOW_2: 9;

        then ((d * g) . (d . t)) <= (d . t);

        then (d . t) >= (((d * g) * d) . t) by FUNCT_2: 15;

        hence thesis by A5, ORDERS_2: 2;

      end;

      hence d = ((d * g) * d) by FUNCT_2: 63;

      for s be Element of S holds (g . s) = (((g * d) * g) . s)

      proof

        let s be Element of S;

        ((d * g) . s) <= (( id S) . s) by A3, YELLOW_2: 9;

        then ((d * g) . s) <= s;

        then (g . ((d * g) . s)) <= (g . s) by A1;

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

        then

         A6: (g . s) >= (((g * d) * g) . s) by RELAT_1: 36;

        (( id T) . (g . s)) <= ((g * d) . (g . s)) by A4, YELLOW_2: 9;

        then (g . s) <= ((g * d) . (g . s));

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

        hence thesis by A6, ORDERS_2: 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: WAYBEL_1:21

    

     Th21: for S,T be non empty RelStr, g be Function of S, T, d be Function of T, S st g = ((g * d) * g) holds (g * d) is idempotent

    proof

      let S,T be non empty RelStr, g be Function of S, T, d be Function of T, S;

      assume g = ((g * d) * g);

      hence ((g * d) * (g * d)) = (g * d) by RELAT_1: 36;

    end;

    theorem :: WAYBEL_1:22

    

     Th22: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st [g, d] is Galois & g is onto holds for t be Element of T holds (d . t) is_minimum_of (g " {t})

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      assume that

       A1: [g, d] is Galois and

       A2: g is onto;

      

       A3: g is monotone by A1, Th8;

      let t be Element of T;

      

       A4: ( rng g) = the carrier of T by A2, FUNCT_2:def 3;

      then

       A5: (g .: (g " ( uparrow t))) = ( uparrow t) by FUNCT_1: 77;

      

       A6: (d . t) is_minimum_of (g " ( uparrow t)) by A1, Th10;

      then

       A7: (d . t) = ( inf (g " ( uparrow t)));

      (d . t) in (g " ( uparrow t)) by A6;

      then (g . (d . t)) in (g .: (g " ( uparrow t))) by FUNCT_2: 35;

      then

       A8: t <= (g . (d . t)) by A5, WAYBEL_0: 18;

       ex_inf_of ((g " ( uparrow t)),S) by A6;

      then

       A9: (d . t) is_<=_than (g " ( uparrow t)) by A7, YELLOW_0: 31;

      consider s be object such that

       A10: s in the carrier of S and

       A11: (g . s) = t by A4, FUNCT_2: 11;

      reconsider s as Element of S by A10;

      

       A12: t in {t} by TARSKI:def 1;

      

       A13: {t} c= ( uparrow {t}) by WAYBEL_0: 16;

      then s in (g " ( uparrow t)) by A11, A12, FUNCT_2: 38;

      then (d . t) <= s by A9;

      then (g . (d . t)) <= t by A11, A3;

      then

       A14: (g . (d . t)) = t by A8, ORDERS_2: 2;

      then

       A15: (d . t) in (g " {t}) by A12, FUNCT_2: 38;

      

       A16: (g " {t}) c= (g " ( uparrow t)) by RELAT_1: 143, WAYBEL_0: 16;

      thus

       A17: ex_inf_of ((g " {t}),S)

      proof

        take (d . t);

        thus (g " {t}) is_>=_than (d . t) by A9, A16;

        thus for b be Element of S st (g " {t}) is_>=_than b holds b <= (d . t) by A15;

        let c be Element of S;

        assume (g " {t}) is_>=_than c;

        then

         A18: c <= (d . t) by A15;

        assume for b be Element of S st (g " {t}) is_>=_than b holds b <= c;

        then (d . t) <= c by A9, A16, YELLOW_0: 9;

        hence thesis by A18, ORDERS_2: 2;

      end;

      then ( inf (g " {t})) is_<=_than (g " {t}) by YELLOW_0: 31;

      then

       A19: ( inf (g " {t})) <= (d . t) by A15;

       ex_inf_of ((g " ( uparrow t)),S) by A6;

      then ( inf (g " {t})) >= (d . t) by A7, A13, A17, RELAT_1: 143, YELLOW_0: 35;

      hence (d . t) = ( inf (g " {t})) by A19, ORDERS_2: 2;

      hence thesis by A12, A14, FUNCT_2: 38;

    end;

    theorem :: WAYBEL_1:23

    

     Th23: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st for t be Element of T holds (d . t) is_minimum_of (g " {t}) holds (g * d) = ( id T)

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      assume

       A1: for t be Element of T holds (d . t) is_minimum_of (g " {t});

      for t be Element of T holds ((g * d) . t) = t

      proof

        let t be Element of T;

        (d . t) is_minimum_of (g " {t}) by A1;

        then (d . t) = ( inf (g " {t})) & ( inf (g " {t})) in (g " {t});

        then (g . (d . t)) in {t} by FUNCT_2: 38;

        then (g . (d . t)) = t by TARSKI:def 1;

        hence thesis by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 124;

    end;

    theorem :: WAYBEL_1:24

    for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st [g, d] is Galois holds g is onto iff d is one-to-one

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      

       A1: the carrier of T = ( dom d) & the carrier of T = ( dom (g * d)) by FUNCT_2:def 1;

      assume

       A2: [g, d] is Galois;

      then

       A3: (d * g) <= ( id S) & ( id T) <= (g * d) by Th18;

      hereby

        assume g is onto;

        then for t be Element of T holds (d . t) is_minimum_of (g " {t}) by A2, Th22;

        then (g * d) = ( id T) by Th23;

        hence d is one-to-one by FUNCT_2: 23;

      end;

      

       A4: ( rng (g * d)) c= the carrier of T;

      g is monotone & d is monotone by A2, Th8;

      

      then

       A5: d = ((d * g) * d) by A3, Th20

      .= (d * (g * d)) by RELAT_1: 36;

      assume d is one-to-one;

      then (g * d) = ( id T) by A1, A4, A5, FUNCT_1: 28;

      hence thesis by FUNCT_2: 23;

    end;

    theorem :: WAYBEL_1:25

    

     Th25: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st [g, d] is Galois & d is onto holds for s be Element of S holds (g . s) is_maximum_of (d " {s})

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      assume that

       A1: [g, d] is Galois and

       A2: d is onto;

      

       A3: d is monotone by A1, Th8;

      let s be Element of S;

      

       A4: ( rng d) = the carrier of S by A2, FUNCT_2:def 3;

      then

       A5: (d .: (d " ( downarrow s))) = ( downarrow s) by FUNCT_1: 77;

      

       A6: (g . s) is_maximum_of (d " ( downarrow s)) by A1, Th11;

      then

       A7: (g . s) = ( sup (d " ( downarrow s)));

      (g . s) in (d " ( downarrow s)) by A6;

      then (d . (g . s)) in (d .: (d " ( downarrow s))) by FUNCT_2: 35;

      then

       A8: s >= (d . (g . s)) by A5, WAYBEL_0: 17;

       ex_sup_of ((d " ( downarrow s)),T) by A6;

      then

       A9: (g . s) is_>=_than (d " ( downarrow s)) by A7, YELLOW_0: 30;

      consider t be object such that

       A10: t in the carrier of T and

       A11: (d . t) = s by A4, FUNCT_2: 11;

      reconsider t as Element of T by A10;

      

       A12: s in {s} by TARSKI:def 1;

      

       A13: {s} c= ( downarrow {s}) by WAYBEL_0: 16;

      then t in (d " ( downarrow s)) by A11, A12, FUNCT_2: 38;

      then (g . s) >= t by A9;

      then (d . (g . s)) >= s by A11, A3;

      then

       A14: (d . (g . s)) = s by A8, ORDERS_2: 2;

      then

       A15: (g . s) in (d " {s}) by A12, FUNCT_2: 38;

      

       A16: (d " {s}) c= (d " ( downarrow s)) by RELAT_1: 143, WAYBEL_0: 16;

      thus

       A17: ex_sup_of ((d " {s}),T)

      proof

        take (g . s);

        thus (d " {s}) is_<=_than (g . s) by A9, A16;

        thus for b be Element of T st (d " {s}) is_<=_than b holds b >= (g . s) by A15;

        let c be Element of T;

        assume (d " {s}) is_<=_than c;

        then

         A18: c >= (g . s) by A15;

        assume for b be Element of T st (d " {s}) is_<=_than b holds b >= c;

        then (g . s) >= c by A9, A16, YELLOW_0: 9;

        hence thesis by A18, ORDERS_2: 2;

      end;

      then ( sup (d " {s})) is_>=_than (d " {s}) by YELLOW_0: 30;

      then

       A19: ( sup (d " {s})) >= (g . s) by A15;

       ex_sup_of ((d " ( downarrow s)),T) by A6;

      then ( sup (d " {s})) <= (g . s) by A7, A13, A17, RELAT_1: 143, YELLOW_0: 34;

      hence (g . s) = ( sup (d " {s})) by A19, ORDERS_2: 2;

      hence thesis by A12, A14, FUNCT_2: 38;

    end;

    theorem :: WAYBEL_1:26

    

     Th26: for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st for s be Element of S holds (g . s) is_maximum_of (d " {s}) holds (d * g) = ( id S)

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      assume

       A1: for s be Element of S holds (g . s) is_maximum_of (d " {s});

      for s be Element of S holds ((d * g) . s) = s

      proof

        let s be Element of S;

        (g . s) is_maximum_of (d " {s}) by A1;

        then (g . s) = ( sup (d " {s})) & ( sup (d " {s})) in (d " {s});

        then (d . (g . s)) in {s} by FUNCT_2: 38;

        then (d . (g . s)) = s by TARSKI:def 1;

        hence thesis by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 124;

    end;

    theorem :: WAYBEL_1:27

    for S,T be non empty Poset, g be Function of S, T, d be Function of T, S st [g, d] is Galois holds g is one-to-one iff d is onto

    proof

      let S,T be non empty Poset, g be Function of S, T, d be Function of T, S;

      assume

       A1: [g, d] is Galois;

      hereby

        

         A2: (d * g) <= ( id S) & ( id T) <= (g * d) by A1, Th18;

        g is monotone & d is monotone by A1, Th8;

        

        then

         A3: g = ((g * d) * g) by A2, Th20

        .= (g * (d * g)) by RELAT_1: 36;

        

         A4: the carrier of S = ( dom g) & the carrier of S = ( dom (d * g)) by FUNCT_2:def 1;

        

         A5: ( rng (d * g)) c= the carrier of S;

        assume g is one-to-one;

        then (d * g) = ( id S) by A4, A5, A3, FUNCT_1: 28;

        hence d is onto by FUNCT_2: 23;

      end;

      assume d is onto;

      then for s be Element of S holds (g . s) is_maximum_of (d " {s}) by A1, Th25;

      then (d * g) = ( id S) by Th26;

      hence thesis by FUNCT_2: 23;

    end;

    definition

      let L be non empty RelStr, p be Function of L, L;

      :: WAYBEL_1:def13

      attr p is projection means

      : Def13: p is idempotent monotone;

    end

    registration

      let L be non empty RelStr;

      cluster ( id L) -> projection;

      coherence by YELLOW_2: 21;

    end

    registration

      let L be non empty RelStr;

      cluster projection for Function of L, L;

      existence

      proof

        take ( id L);

        thus thesis;

      end;

    end

    definition

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

      :: WAYBEL_1:def14

      attr c is closure means c is projection & ( id L) <= c;

    end

    registration

      let L be non empty RelStr;

      cluster closure -> projection for Function of L, L;

      coherence ;

    end

    

     Lm1: for L1,L2 be non empty RelStr, f be Function of L1, L2 st L2 is reflexive holds f <= f

    proof

      let L1,L2 be non empty RelStr, f be Function of L1, L2;

      assume L2 is reflexive;

      then for x be Element of L1 holds (f . x) <= (f . x);

      hence thesis by YELLOW_2: 9;

    end;

    registration

      let L be non empty reflexive RelStr;

      cluster closure for Function of L, L;

      existence

      proof

        take ( id L);

        thus ( id L) is projection;

        thus thesis by Lm1;

      end;

    end

    registration

      let L be non empty reflexive RelStr;

      cluster ( id L) -> closure;

      coherence by Lm1;

    end

    definition

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

      :: WAYBEL_1:def15

      attr k is kernel means k is projection & k <= ( id L);

    end

    registration

      let L be non empty RelStr;

      cluster kernel -> projection for Function of L, L;

      coherence ;

    end

    registration

      let L be non empty reflexive RelStr;

      cluster kernel for Function of L, L;

      existence

      proof

        take ( id L);

        thus ( id L) is projection;

        thus thesis by Lm1;

      end;

    end

    registration

      let L be non empty reflexive RelStr;

      cluster ( id L) -> kernel;

      coherence by Lm1;

    end

    

     Lm2: for L be non empty 1-sorted, p be Function of L, L st p is idempotent holds for x be set st x in ( rng p) holds (p . x) = x

    proof

      let L be non empty 1-sorted, p be Function of L, L such that

       A1: p is idempotent;

      let x be set;

      assume x in ( rng p);

      then ex a be object st a in ( dom p) & x = (p . a) by FUNCT_1:def 3;

      hence thesis by A1, YELLOW_2: 18;

    end;

    theorem :: WAYBEL_1:28

    

     Th28: for L be non empty Poset, c be Function of L, L, X be Subset of L st c is closure & ex_inf_of (X,L) & X c= ( rng c) holds ( inf X) = (c . ( inf X))

    proof

      let L be non empty Poset, c be Function of L, L, X be Subset of L such that

       A1: c is projection and

       A2: ( id L) <= c and

       A3: ex_inf_of (X,L) and

       A4: X c= ( rng c);

      

       A5: c is monotone by A1;

      

       A6: c is idempotent by A1;

      (c . ( inf X)) is_<=_than X

      proof

        let x be Element of L;

        assume

         A7: x in X;

        ( inf X) is_<=_than X by A3, YELLOW_0: 31;

        then ( inf X) <= x by A7;

        then (c . ( inf X)) <= (c . x) by A5;

        hence thesis by A4, A6, A7, Lm2;

      end;

      then

       A8: (c . ( inf X)) <= ( inf X) by A3, YELLOW_0: 31;

      (( id L) . ( inf X)) <= (c . ( inf X)) by A2, YELLOW_2: 9;

      then ( inf X) <= (c . ( inf X));

      hence thesis by A8, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_1:29

    

     Th29: for L be non empty Poset, k be Function of L, L, X be Subset of L st k is kernel & ex_sup_of (X,L) & X c= ( rng k) holds ( sup X) = (k . ( sup X))

    proof

      let L be non empty Poset, k be Function of L, L, X be Subset of L such that

       A1: k is projection and

       A2: k <= ( id L) and

       A3: ex_sup_of (X,L) and

       A4: X c= ( rng k);

      

       A5: k is monotone by A1;

      

       A6: k is idempotent by A1;

      (k . ( sup X)) is_>=_than X

      proof

        let x be Element of L;

        assume

         A7: x in X;

        ( sup X) is_>=_than X by A3, YELLOW_0: 30;

        then ( sup X) >= x by A7;

        then (k . ( sup X)) >= (k . x) by A5;

        hence thesis by A4, A6, A7, Lm2;

      end;

      then

       A8: (k . ( sup X)) >= ( sup X) by A3, YELLOW_0: 30;

      (( id L) . ( sup X)) >= (k . ( sup X)) by A2, YELLOW_2: 9;

      then ( sup X) >= (k . ( sup X));

      hence thesis by A8, ORDERS_2: 2;

    end;

    definition

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

      :: WAYBEL_1:def16

      func corestr (g) -> Function of L1, ( Image g) equals (the carrier of ( Image g) |` g);

      coherence

      proof

        

         A1: the carrier of L1 = ( dom g) by FUNCT_2:def 1;

        

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

        thus thesis by A2, A1, FUNCT_2: 1;

      end;

    end

    theorem :: WAYBEL_1:30

    

     Th30: for L1,L2 be non empty RelStr, g be Function of L1, L2 holds ( corestr g) = g

    proof

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

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

      hence thesis;

    end;

    

     Lm3: for L1,L2 be non empty RelStr, g be Function of L1, L2 holds ( corestr g) is onto

    proof

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

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

      .= ( rng ( corestr g)) by Th30;

      hence thesis by FUNCT_2:def 3;

    end;

    registration

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

      cluster ( corestr g) -> onto;

      coherence by Lm3;

    end

    theorem :: WAYBEL_1:31

    

     Th31: for L1,L2 be non empty RelStr, g be Function of L1, L2 st g is monotone holds ( corestr g) is monotone

    proof

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

       A1: g is monotone;

      let s1,s2 be Element of L1;

      assume s1 <= s2;

      then

       A2: (g . s1) <= (g . s2) by A1;

      reconsider s19 = (g . s1), s29 = (g . s2) as Element of L2;

      s19 = (( corestr g) . s1) & s29 = (( corestr g) . s2) by Th30;

      hence thesis by A2, YELLOW_0: 60;

    end;

    definition

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

      :: WAYBEL_1:def17

      func inclusion (g) -> Function of ( Image g), L2 equals ( id ( Image g));

      coherence

      proof

        

         A1: ( rng ( id ( Image g))) = the carrier of ( Image g)

        .= ( rng g) by YELLOW_0:def 15;

        ( dom ( id ( Image g))) = the carrier of ( Image g);

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    

     Lm4: for L1,L2 be non empty RelStr, g be Function of L1, L2 holds ( inclusion g) is monotone by YELLOW_0: 59;

    registration

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

      cluster ( inclusion g) -> one-to-one monotone;

      coherence by Lm4;

    end

    theorem :: WAYBEL_1:32

    

     Th32: for L be non empty RelStr, f be Function of L, L holds (( inclusion f) * ( corestr f)) = f

    proof

      let L be non empty RelStr, f be Function of L, L;

      

      thus (( inclusion f) * ( corestr f)) = (( id the carrier of ( Image f)) * f) by Th30

      .= (( id ( rng f)) * f) by YELLOW_0:def 15

      .= f by RELAT_1: 54;

    end;

    theorem :: WAYBEL_1:33

    

     Th33: for L be non empty Poset, f be Function of L, L st f is idempotent holds (( corestr f) * ( inclusion f)) = ( id ( Image f))

    proof

      let L be non empty Poset, f be Function of L, L;

      assume

       A1: f is idempotent;

      for s be Element of ( Image f) holds ((( corestr f) * ( inclusion f)) . s) = s

      proof

        let s be Element of ( Image f);

        the carrier of ( Image f) = ( rng ( corestr f)) by FUNCT_2:def 3;

        then

        consider l be object such that

         A2: l in the carrier of L and

         A3: (( corestr f) . l) = s by FUNCT_2: 11;

        reconsider l as Element of L by A2;

        

         A4: (( corestr f) . l) = (f . l) by Th30;

        

        thus ((( corestr f) * ( inclusion f)) . s) = (( corestr f) . (( inclusion f) . s)) by FUNCT_2: 15

        .= (( corestr f) . s)

        .= (f . (f . l)) by A3, A4, Th30

        .= s by A1, A3, A4, YELLOW_2: 18;

      end;

      hence thesis by FUNCT_2: 124;

    end;

    theorem :: WAYBEL_1:34

    for L be non empty Poset, f be Function of L, L st f is projection holds ex T be non empty Poset, q be Function of L, T, i be Function of T, L st q is monotone & q is onto & i is monotone & i is one-to-one & f = (i * q) & ( id T) = (q * i)

    proof

      let L be non empty Poset, f be Function of L, L;

      reconsider T = ( Image f) as non empty Poset;

      reconsider q = ( corestr f) as Function of L, T;

      reconsider i = ( inclusion f) as Function of T, L;

      assume f is projection;

      then

       A1: f is monotone idempotent;

      take T, q, i;

      thus q is monotone by A1, Th31;

      thus q is onto;

      thus i is monotone one-to-one;

      thus f = (i * q) by Th32;

      thus thesis by A1, Th33;

    end;

    theorem :: WAYBEL_1:35

    for L be non empty Poset, f be Function of L, L st (ex T be non empty Poset, q be Function of L, T, i be Function of T, L st q is monotone & i is monotone & f = (i * q) & ( id T) = (q * i)) holds f is projection

    proof

      let L be non empty Poset, f be Function of L, L;

      given T be non empty Poset, q be Function of L, T, i be Function of T, L such that

       A1: q is monotone & i is monotone and

       A2: f = (i * q) and

       A3: ( id T) = (q * i);

      ((i * q) * i) = (i * ( id the carrier of T)) by A3, RELAT_1: 36

      .= i by FUNCT_2: 17;

      hence f is idempotent by A2, Th21;

      thus thesis by A1, A2, YELLOW_2: 12;

    end;

    theorem :: WAYBEL_1:36

    

     Th36: for L be non empty Poset, f be Function of L, L st f is closure holds [( inclusion f), ( corestr f)] is Galois

    proof

      let L be non empty Poset, f be Function of L, L;

      assume that

       A1: f is idempotent monotone and

       A2: ( id L) <= f;

      set g = ( corestr f), d = ( inclusion f);

      (g * d) = ( id ( Image f)) by A1, Th33;

      then

       A3: (g * d) <= ( id ( Image f)) by Lm1;

      g is monotone & ( id L) <= (d * g) by A1, A2, Th31, Th32;

      hence thesis by A3, Th19;

    end;

    theorem :: WAYBEL_1:37

    for L be non empty Poset, f be Function of L, L st f is closure holds ex S be non empty Poset, g be Function of S, L, d be Function of L, S st [g, d] is Galois & f = (g * d)

    proof

      let L be non empty Poset, f be Function of L, L;

      assume

       A1: f is closure;

      reconsider S = ( Image f) as non empty Poset;

      reconsider g = ( inclusion f) as Function of S, L;

      reconsider d = ( corestr f) as Function of L, S;

      take S, g, d;

      thus [g, d] is Galois by A1, Th36;

      thus thesis by Th32;

    end;

    theorem :: WAYBEL_1:38

    

     Th38: for L be non empty Poset, f be Function of L, L st f is monotone & ex S be non empty Poset, g be Function of S, L, d be Function of L, S st [g, d] is Galois & f = (g * d) holds f is closure

    proof

      let L be non empty Poset, f be Function of L, L such that

       A1: f is monotone;

      given S be non empty Poset, g be Function of S, L, d be Function of L, S such that

       A2: [g, d] is Galois and

       A3: f = (g * d);

      

       A4: d is monotone & g is monotone by A2, Th8;

      (d * g) <= ( id S) & ( id L) <= (g * d) by A2, Th18;

      then g = ((g * d) * g) by A4, Th20;

      hence f is idempotent monotone by A1, A3, Th21;

      thus thesis by A2, A3, Th18;

    end;

    theorem :: WAYBEL_1:39

    

     Th39: for L be non empty Poset, f be Function of L, L st f is kernel holds [( corestr f), ( inclusion f)] is Galois

    proof

      let L be non empty Poset, f be Function of L, L;

      assume that

       A1: f is idempotent monotone and

       A2: f <= ( id L);

      set g = ( corestr f), d = ( inclusion f);

      (g * d) = ( id ( Image f)) by A1, Th33;

      then

       A3: ( id ( Image f)) <= (g * d) by Lm1;

      g is monotone & (d * g) <= ( id L) by A1, A2, Th31, Th32;

      hence thesis by A3, Th19;

    end;

    theorem :: WAYBEL_1:40

    for L be non empty Poset, f be Function of L, L st f is kernel holds ex T be non empty Poset, g be Function of L, T, d be Function of T, L st [g, d] is Galois & f = (d * g)

    proof

      let L be non empty Poset, f be Function of L, L;

      assume

       A1: f is kernel;

      reconsider T = ( Image f) as non empty Poset;

      reconsider g = ( corestr f) as Function of L, T;

      reconsider d = ( inclusion f) as Function of T, L;

      take T, g, d;

      thus [g, d] is Galois by A1, Th39;

      thus thesis by Th32;

    end;

    theorem :: WAYBEL_1:41

    for L be non empty Poset, f be Function of L, L st f is monotone & ex T be non empty Poset, g be Function of L, T, d be Function of T, L st [g, d] is Galois & f = (d * g) holds f is kernel

    proof

      let L be non empty Poset, f be Function of L, L;

      assume

       A1: f is monotone;

      given T be non empty Poset, g be Function of L, T, d be Function of T, L such that

       A2: [g, d] is Galois and

       A3: f = (d * g);

      

       A4: d is monotone & g is monotone by A2, Th8;

      (d * g) <= ( id L) & ( id T) <= (g * d) by A2, Th18;

      then d = ((d * g) * d) by A4, Th20;

      hence f is idempotent monotone by A1, A3, Th21;

      thus thesis by A2, A3, Th18;

    end;

    theorem :: WAYBEL_1:42

    

     Th42: for L be non empty Poset, p be Function of L, L st p is projection holds ( rng p) = ({ c where c be Element of L : c <= (p . c) } /\ { k where k be Element of L : (p . k) <= k })

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is idempotent and p is monotone;

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

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

      thus ( rng p) c= (Lc /\ Lk)

      proof

        let x be object;

        assume

         A2: x in ( rng p);

        then

        reconsider x9 = x as Element of L;

        

         A3: ex l be object st l in ( dom p) & (p . l) = x by A2, FUNCT_1:def 3;

        then (p . x9) <= x9 by A1, YELLOW_2: 18;

        then

         A4: x in Lk;

        x9 <= (p . x9) by A1, A3, YELLOW_2: 18;

        then x in Lc;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A5: x in (Lc /\ Lk);

      then x in Lc by XBOOLE_0:def 4;

      then

       A6: ex lc be Element of L st x = lc & lc <= (p . lc);

      x in Lk by A5, XBOOLE_0:def 4;

      then ex lk be Element of L st x = lk & (p . lk) <= lk;

      then ( dom p) = the carrier of L & x = (p . x) by A6, FUNCT_2:def 1, ORDERS_2: 2;

      hence thesis by A6, FUNCT_1:def 3;

    end;

    theorem :: WAYBEL_1:43

    

     Th43: for L be non empty Poset, p be Function of L, L st p is projection holds { c where c be Element of L : c <= (p . c) } is non empty Subset of L & { k where k be Element of L : (p . k) <= k } is non empty Subset of L

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is projection;

      defpred Q[ Element of L] means (p . $1) <= $1;

      defpred P[ Element of L] means $1 <= (p . $1);

      set Lc = { c where c be Element of L : P[c] };

      set Lk = { k where k be Element of L : Q[k] };

      

       A2: ( rng p) = (Lc /\ Lk) by A1, Th42;

      Lc is Subset of L from DOMAIN_1:sch 7;

      hence Lc is non empty Subset of L by A2;

      Lk is Subset of L from DOMAIN_1:sch 7;

      hence thesis by A2;

    end;

    theorem :: WAYBEL_1:44

    

     Th44: for L be non empty Poset, p be Function of L, L st p is projection holds ( rng (p | { c where c be Element of L : c <= (p . c) })) = ( rng p) & ( rng (p | { k where k be Element of L : (p . k) <= k })) = ( rng p)

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is projection;

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

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

      

       A2: ( rng p) = (Lc /\ Lk) by A1, Th42;

      

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

      thus ( rng (p | Lc)) = ( rng p)

      proof

        thus ( rng (p | Lc)) c= ( rng p) by RELAT_1: 70;

        let y be object;

        assume

         A4: y in ( rng p);

        then

         A5: y in Lc by A2, XBOOLE_0:def 4;

        then

         A6: ex lc be Element of L st y = lc & lc <= (p . lc);

        y in Lk by A2, A4, XBOOLE_0:def 4;

        then ex lk be Element of L st y = lk & (p . lk) <= lk;

        then y = (p . y) by A6, ORDERS_2: 2;

        hence thesis by A3, A5, A6, FUNCT_1: 50;

      end;

      thus ( rng (p | Lk)) c= ( rng p) by RELAT_1: 70;

      let y be object;

      assume

       A7: y in ( rng p);

      then y in Lc by A2, XBOOLE_0:def 4;

      then

       A8: ex lc be Element of L st y = lc & lc <= (p . lc);

      

       A9: y in Lk by A2, A7, XBOOLE_0:def 4;

      then ex lk be Element of L st y = lk & (p . lk) <= lk;

      then y = (p . y) by A8, ORDERS_2: 2;

      hence thesis by A3, A9, A8, FUNCT_1: 50;

    end;

    theorem :: WAYBEL_1:45

    

     Th45: for L be non empty Poset, p be Function of L, L st p is projection holds for Lc be non empty Subset of L, Lk be non empty Subset of L st Lc = { c where c be Element of L : c <= (p . c) } holds (p | Lc) is Function of ( subrelstr Lc), ( subrelstr Lc)

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is projection;

      let Lc be non empty Subset of L, Lk be non empty Subset of L such that

       A2: Lc = { c where c be Element of L : c <= (p . c) };

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

      ( rng p) = (Lc /\ Lk) by A1, A2, Th42;

      then ( rng (p | Lc)) = (Lc /\ Lk) by A1, A2, Th44;

      then

       A3: ( rng (p | Lc)) c= Lc by XBOOLE_1: 17;

      Lc = the carrier of ( subrelstr Lc) & (p | Lc) is Function of Lc, the carrier of L by FUNCT_2: 32, YELLOW_0:def 15;

      hence thesis by A3, FUNCT_2: 6;

    end;

    theorem :: WAYBEL_1:46

    for L be non empty Poset, p be Function of L, L st p is projection holds for Lk be non empty Subset of L st Lk = { k where k be Element of L : (p . k) <= k } holds (p | Lk) is Function of ( subrelstr Lk), ( subrelstr Lk)

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is projection;

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

      let Lk be non empty Subset of L such that

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

      ( rng p) = (Lc /\ Lk) by A1, A2, Th42;

      then ( rng (p | Lk)) = (Lc /\ Lk) by A1, A2, Th44;

      then

       A3: ( rng (p | Lk)) c= Lk by XBOOLE_1: 17;

      Lk = the carrier of ( subrelstr Lk) & (p | Lk) is Function of Lk, the carrier of L by FUNCT_2: 32, YELLOW_0:def 15;

      hence thesis by A3, FUNCT_2: 6;

    end;

    theorem :: WAYBEL_1:47

    

     Th47: for L be non empty Poset, p be Function of L, L st p is projection holds for Lc be non empty Subset of L st Lc = { c where c be Element of L : c <= (p . c) } holds for pc be Function of ( subrelstr Lc), ( subrelstr Lc) st pc = (p | Lc) holds pc is closure

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is idempotent and

       A2: p is monotone;

      let Lc be non empty Subset of L such that

       A3: Lc = { c where c be Element of L : c <= (p . c) };

      let pc be Function of ( subrelstr Lc), ( subrelstr Lc) such that

       A4: pc = (p | Lc);

      

       A5: ( dom pc) = the carrier of ( subrelstr Lc) by FUNCT_2:def 1;

      hereby

        now

          let x be Element of ( subrelstr Lc);

          

           A6: x is Element of L by YELLOW_0: 58;

          

           A7: (pc . x) = (p . x) by A4, A5, FUNCT_1: 47;

          

          then (p . (p . x)) = (pc . (pc . x)) by A4, A5, FUNCT_1: 47

          .= ((pc * pc) . x) by A5, FUNCT_1: 13;

          hence ((pc * pc) . x) = (pc . x) by A1, A7, A6, YELLOW_2: 18;

        end;

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

        thus pc is monotone

        proof

          let x1,x2 be Element of ( subrelstr Lc);

          reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0: 58;

          assume x1 <= x2;

          then x19 <= x29 by YELLOW_0: 59;

          then

           A8: (p . x19) <= (p . x29) by A2;

          (pc . x1) = (p . x19) & (pc . x2) = (p . x29) by A4, A5, FUNCT_1: 47;

          hence thesis by A8, YELLOW_0: 60;

        end;

      end;

      now

        let x be Element of ( subrelstr Lc);

        reconsider x9 = x as Element of L by YELLOW_0: 58;

        x in the carrier of ( subrelstr Lc);

        then x in Lc by YELLOW_0:def 15;

        then

         A9: ex c be Element of L st x = c & c <= (p . c) by A3;

        (pc . x) = (p . x9) by A4, A5, FUNCT_1: 47;

        then x <= (pc . x) by A9, YELLOW_0: 60;

        hence (( id ( subrelstr Lc)) . x) <= (pc . x);

      end;

      hence thesis by YELLOW_2: 9;

    end;

    theorem :: WAYBEL_1:48

    for L be non empty Poset, p be Function of L, L st p is projection holds for Lk be non empty Subset of L st Lk = { k where k be Element of L : (p . k) <= k } holds for pk be Function of ( subrelstr Lk), ( subrelstr Lk) st pk = (p | Lk) holds pk is kernel

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is idempotent and

       A2: p is monotone;

      let Lk be non empty Subset of L such that

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

      let pk be Function of ( subrelstr Lk), ( subrelstr Lk) such that

       A4: pk = (p | Lk);

      

       A5: ( dom pk) = the carrier of ( subrelstr Lk) by FUNCT_2:def 1;

      hereby

        now

          let x be Element of ( subrelstr Lk);

          

           A6: x is Element of L by YELLOW_0: 58;

          

           A7: (pk . x) = (p . x) by A4, A5, FUNCT_1: 47;

          

          then (p . (p . x)) = (pk . (pk . x)) by A4, A5, FUNCT_1: 47

          .= ((pk * pk) . x) by A5, FUNCT_1: 13;

          hence ((pk * pk) . x) = (pk . x) by A1, A7, A6, YELLOW_2: 18;

        end;

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

        thus pk is monotone

        proof

          let x1,x2 be Element of ( subrelstr Lk);

          reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0: 58;

          assume x1 <= x2;

          then x19 <= x29 by YELLOW_0: 59;

          then

           A8: (p . x19) <= (p . x29) by A2;

          (pk . x1) = (p . x19) & (pk . x2) = (p . x29) by A4, A5, FUNCT_1: 47;

          hence thesis by A8, YELLOW_0: 60;

        end;

      end;

      now

        let x be Element of ( subrelstr Lk);

        reconsider x9 = x as Element of L by YELLOW_0: 58;

        x in the carrier of ( subrelstr Lk);

        then x in Lk by YELLOW_0:def 15;

        then

         A9: ex c be Element of L st x = c & (p . c) <= c by A3;

        (pk . x) = (p . x9) by A4, A5, FUNCT_1: 47;

        then (pk . x) <= x by A9, YELLOW_0: 60;

        hence (pk . x) <= (( id ( subrelstr Lk)) . x);

      end;

      hence thesis by YELLOW_2: 9;

    end;

    theorem :: WAYBEL_1:49

    

     Th49: for L be non empty Poset, p be Function of L, L st p is monotone holds for Lc be Subset of L st Lc = { c where c be Element of L : c <= (p . c) } holds ( subrelstr Lc) is sups-inheriting

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is monotone;

      let Lc be Subset of L such that

       A2: Lc = { c where c be Element of L : c <= (p . c) };

      let X be Subset of ( subrelstr Lc);

      assume

       A3: ex_sup_of (X,L);

      (p . ( "\/" (X,L))) is_>=_than X

      proof

        let x be Element of L;

        assume

         A4: x in X;

        then x in the carrier of ( subrelstr Lc);

        then x in Lc by YELLOW_0:def 15;

        then

         A5: ex l be Element of L st x = l & l <= (p . l) by A2;

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

        then x <= ( "\/" (X,L)) by A4;

        then (p . x) <= (p . ( "\/" (X,L))) by A1;

        hence x <= (p . ( "\/" (X,L))) by A5, ORDERS_2: 3;

      end;

      then ( "\/" (X,L)) <= (p . ( "\/" (X,L))) by A3, YELLOW_0: 30;

      then ( "\/" (X,L)) in Lc by A2;

      hence thesis by YELLOW_0:def 15;

    end;

    theorem :: WAYBEL_1:50

    

     Th50: for L be non empty Poset, p be Function of L, L st p is monotone holds for Lk be Subset of L st Lk = { k where k be Element of L : (p . k) <= k } holds ( subrelstr Lk) is infs-inheriting

    proof

      let L be non empty Poset, p be Function of L, L such that

       A1: p is monotone;

      let Lk be Subset of L such that

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

      let X be Subset of ( subrelstr Lk);

      assume

       A3: ex_inf_of (X,L);

      (p . ( "/\" (X,L))) is_<=_than X

      proof

        let x be Element of L;

        assume

         A4: x in X;

        then x in the carrier of ( subrelstr Lk);

        then x in Lk by YELLOW_0:def 15;

        then

         A5: ex l be Element of L st x = l & l >= (p . l) by A2;

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

        then x >= ( "/\" (X,L)) by A4;

        then (p . x) >= (p . ( "/\" (X,L))) by A1;

        hence thesis by A5, ORDERS_2: 3;

      end;

      then ( "/\" (X,L)) >= (p . ( "/\" (X,L))) by A3, YELLOW_0: 31;

      then ( "/\" (X,L)) in Lk by A2;

      hence thesis by YELLOW_0:def 15;

    end;

    theorem :: WAYBEL_1:51

    for L be non empty Poset, p be Function of L, L st p is projection holds for Lc be non empty Subset of L st Lc = { c where c be Element of L : c <= (p . c) } holds (p is infs-preserving implies ( subrelstr Lc) is infs-inheriting & ( Image p) is infs-inheriting) & (p is filtered-infs-preserving implies ( subrelstr Lc) is filtered-infs-inheriting & ( Image p) is filtered-infs-inheriting)

    proof

      let L be non empty Poset, p be Function of L, L;

      assume

       A1: p is projection;

      then

      reconsider Lk = { k where k be Element of L : (p . k) <= k } as non empty Subset of L by Th43;

      let Lc be non empty Subset of L such that

       A2: Lc = { c where c be Element of L : c <= (p . c) };

      

       A3: p is monotone by A1;

      then

       A4: ( subrelstr Lk) is infs-inheriting by Th50;

      

       A5: Lc = the carrier of ( subrelstr Lc) by YELLOW_0:def 15;

      

       A6: the carrier of ( Image p) = ( rng p) by YELLOW_0:def 15

      .= (Lc /\ Lk) by A1, A2, Th42;

      then

       A7: the carrier of ( Image p) c= Lk by XBOOLE_1: 17;

      

       A8: Lk = the carrier of ( subrelstr Lk) by YELLOW_0:def 15;

      

       A9: the carrier of ( Image p) c= Lc by A6, XBOOLE_1: 17;

      hereby

        assume

         A10: p is infs-preserving;

        thus

         A11: ( subrelstr Lc) is infs-inheriting

        proof

          let X be Subset of ( subrelstr Lc);

          the carrier of ( subrelstr Lc) is Subset of L by YELLOW_0:def 15;

          then

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

          assume

           A12: ex_inf_of (X,L);

          

           A13: ( inf X9) is_<=_than (p .: X9)

          proof

            let y be Element of L;

            assume y in (p .: X9);

            then

            consider x be Element of L such that

             A14: x in X9 and

             A15: y = (p . x) by FUNCT_2: 65;

            reconsider x as Element of L;

            x in Lc by A5, A14;

            then

             A16: ex x9 be Element of L st x9 = x & x9 <= (p . x9) by A2;

            ( inf X9) is_<=_than X9 by A12, YELLOW_0: 31;

            then ( inf X9) <= x by A14;

            hence ( inf X9) <= y by A15, A16, ORDERS_2: 3;

          end;

          p preserves_inf_of X9 by A10;

          then ex_inf_of ((p .: X),L) & ( inf (p .: X9)) = (p . ( inf X9)) by A12;

          then ( inf X9) <= (p . ( inf X9)) by A13, YELLOW_0: 31;

          hence thesis by A2, A5;

        end;

        thus ( Image p) is infs-inheriting

        proof

          let X be Subset of ( Image p) such that

           A17: ex_inf_of (X,L);

          X c= Lc by A9;

          then

           A18: ( "/\" (X,L)) in the carrier of ( subrelstr Lc) by A5, A11, A17;

          ( subrelstr Lk) is infs-inheriting & X c= the carrier of ( subrelstr Lk) by A3, A7, A8, Th50;

          then ( "/\" (X,L)) in the carrier of ( subrelstr Lk) by A17;

          hence thesis by A6, A5, A8, A18, XBOOLE_0:def 4;

        end;

      end;

      assume

       A19: p is filtered-infs-preserving;

      thus

       A20: ( subrelstr Lc) is filtered-infs-inheriting

      proof

        let X be filtered Subset of ( subrelstr Lc);

        assume X <> {} ;

        then

        reconsider X9 = X as non empty filtered Subset of L by YELLOW_2: 7;

        assume

         A21: ex_inf_of (X,L);

        

         A22: ( inf X9) is_<=_than (p .: X9)

        proof

          let y be Element of L;

          assume y in (p .: X9);

          then

          consider x be Element of L such that

           A23: x in X9 and

           A24: y = (p . x) by FUNCT_2: 65;

          reconsider x as Element of L;

          x in Lc by A5, A23;

          then

           A25: ex x9 be Element of L st x9 = x & x9 <= (p . x9) by A2;

          ( inf X9) is_<=_than X9 by A21, YELLOW_0: 31;

          then ( inf X9) <= x by A23;

          hence ( inf X9) <= y by A24, A25, ORDERS_2: 3;

        end;

        p preserves_inf_of X9 by A19;

        then ex_inf_of ((p .: X),L) & ( inf (p .: X9)) = (p . ( inf X9)) by A21;

        then ( inf X9) <= (p . ( inf X9)) by A22, YELLOW_0: 31;

        hence thesis by A2, A5;

      end;

      let X be filtered Subset of ( Image p) such that

       A26: X <> {} and

       A27: ex_inf_of (X,L);

      the carrier of ( Image p) c= the carrier of ( subrelstr Lc) by A9, YELLOW_0:def 15;

      then X is filtered Subset of ( subrelstr Lc) by YELLOW_2: 8;

      then

       A28: ( "/\" (X,L)) in the carrier of ( subrelstr Lc) by A20, A26, A27;

      X c= the carrier of ( subrelstr Lk) by A7, A8;

      then ( "/\" (X,L)) in the carrier of ( subrelstr Lk) by A27, A4;

      hence thesis by A6, A5, A8, A28, XBOOLE_0:def 4;

    end;

    theorem :: WAYBEL_1:52

    for L be non empty Poset, p be Function of L, L st p is projection holds for Lk be non empty Subset of L st Lk = { k where k be Element of L : (p . k) <= k } holds (p is sups-preserving implies ( subrelstr Lk) is sups-inheriting & ( Image p) is sups-inheriting) & (p is directed-sups-preserving implies ( subrelstr Lk) is directed-sups-inheriting & ( Image p) is directed-sups-inheriting)

    proof

      let L be non empty Poset, p be Function of L, L;

      assume

       A1: p is projection;

      then

      reconsider Lc = { c where c be Element of L : c <= (p . c) } as non empty Subset of L by Th43;

      let Lk be non empty Subset of L such that

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

      

       A3: p is monotone by A1;

      then

       A4: ( subrelstr Lc) is sups-inheriting by Th49;

      

       A5: Lc = the carrier of ( subrelstr Lc) by YELLOW_0:def 15;

      

       A6: the carrier of ( Image p) = ( rng p) by YELLOW_0:def 15

      .= (Lc /\ Lk) by A1, A2, Th42;

      then

       A7: the carrier of ( Image p) c= Lk by XBOOLE_1: 17;

      

       A8: Lk = the carrier of ( subrelstr Lk) by YELLOW_0:def 15;

      

       A9: the carrier of ( Image p) c= Lc by A6, XBOOLE_1: 17;

      hereby

        assume

         A10: p is sups-preserving;

        thus

         A11: ( subrelstr Lk) is sups-inheriting

        proof

          let X be Subset of ( subrelstr Lk);

          the carrier of ( subrelstr Lk) is Subset of L by YELLOW_0:def 15;

          then

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

          assume

           A12: ex_sup_of (X,L);

          

           A13: ( sup X9) is_>=_than (p .: X9)

          proof

            let y be Element of L;

            assume y in (p .: X9);

            then

            consider x be Element of L such that

             A14: x in X9 and

             A15: y = (p . x) by FUNCT_2: 65;

            reconsider x as Element of L;

            x in Lk by A8, A14;

            then

             A16: ex x9 be Element of L st x9 = x & x9 >= (p . x9) by A2;

            ( sup X9) is_>=_than X9 by A12, YELLOW_0: 30;

            then ( sup X9) >= x by A14;

            hence thesis by A15, A16, ORDERS_2: 3;

          end;

          p preserves_sup_of X9 by A10;

          then ex_sup_of ((p .: X),L) & ( sup (p .: X9)) = (p . ( sup X9)) by A12;

          then ( sup X9) >= (p . ( sup X9)) by A13, YELLOW_0: 30;

          hence thesis by A2, A8;

        end;

        thus ( Image p) is sups-inheriting

        proof

          let X be Subset of ( Image p) such that

           A17: ex_sup_of (X,L);

          X c= Lk by A7;

          then

           A18: ( "\/" (X,L)) in the carrier of ( subrelstr Lk) by A8, A11, A17;

          ( subrelstr Lc) is sups-inheriting & X c= the carrier of ( subrelstr Lc) by A3, A9, A5, Th49;

          then ( "\/" (X,L)) in the carrier of ( subrelstr Lc) by A17;

          hence thesis by A6, A5, A8, A18, XBOOLE_0:def 4;

        end;

      end;

      assume

       A19: p is directed-sups-preserving;

      thus

       A20: ( subrelstr Lk) is directed-sups-inheriting

      proof

        let X be directed Subset of ( subrelstr Lk);

        assume X <> {} ;

        then

        reconsider X9 = X as non empty directed Subset of L by YELLOW_2: 7;

        assume

         A21: ex_sup_of (X,L);

        

         A22: ( sup X9) is_>=_than (p .: X9)

        proof

          let y be Element of L;

          assume y in (p .: X9);

          then

          consider x be Element of L such that

           A23: x in X9 and

           A24: y = (p . x) by FUNCT_2: 65;

          reconsider x as Element of L;

          x in Lk by A8, A23;

          then

           A25: ex x9 be Element of L st x9 = x & x9 >= (p . x9) by A2;

          ( sup X9) is_>=_than X9 by A21, YELLOW_0: 30;

          then ( sup X9) >= x by A23;

          hence thesis by A24, A25, ORDERS_2: 3;

        end;

        p preserves_sup_of X9 by A19;

        then ex_sup_of ((p .: X),L) & ( sup (p .: X9)) = (p . ( sup X9)) by A21;

        then ( sup X9) >= (p . ( sup X9)) by A22, YELLOW_0: 30;

        hence thesis by A2, A8;

      end;

      let X be directed Subset of ( Image p) such that

       A26: X <> {} and

       A27: ex_sup_of (X,L);

      the carrier of ( Image p) c= the carrier of ( subrelstr Lk) by A7, YELLOW_0:def 15;

      then X is directed Subset of ( subrelstr Lk) by YELLOW_2: 8;

      then

       A28: ( "\/" (X,L)) in the carrier of ( subrelstr Lk) by A20, A26, A27;

      X c= the carrier of ( subrelstr Lc) by A9, A5;

      then ( "\/" (X,L)) in the carrier of ( subrelstr Lc) by A27, A4;

      hence thesis by A6, A5, A8, A28, XBOOLE_0:def 4;

    end;

    theorem :: WAYBEL_1:53

    

     Th53: for L be non empty Poset, p be Function of L, L holds (p is closure implies ( Image p) is infs-inheriting) & (p is kernel implies ( Image p) is sups-inheriting)

    proof

      let L be non empty Poset, p be Function of L, L;

      hereby

        assume

         A1: p is closure;

        thus ( Image p) is infs-inheriting

        proof

          let X be Subset of ( Image p);

          

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

          then

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

          assume ex_inf_of (X,L);

          then (p . ( "/\" (X9,L))) = ( "/\" (X9,L)) by A1, A2, Th28;

          hence thesis by A2, FUNCT_2: 4;

        end;

      end;

      assume

       A3: p is kernel;

      let X be Subset of ( Image p);

      

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

      then

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

      assume ex_sup_of (X,L);

      then (p . ( "\/" (X9,L))) = ( "\/" (X9,L)) by A3, A4, Th29;

      hence thesis by A4, FUNCT_2: 4;

    end;

    theorem :: WAYBEL_1:54

    for L be complete non empty Poset, p be Function of L, L st p is projection holds ( Image p) is complete

    proof

      let L be complete non empty Poset, p be Function of L, L;

      

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

      assume

       A2: p is projection;

      then

      reconsider Lc = { c where c be Element of L : c <= (p . c) }, Lk = { k where k be Element of L : (p . k) <= k } as non empty Subset of L by Th43;

      

       A3: the carrier of ( subrelstr Lc) = Lc & ( rng p) = (Lc /\ Lk) by A2, Th42, YELLOW_0:def 15;

      p is monotone by A2;

      then ( subrelstr Lc) is sups-inheriting by Th49;

      then

       A4: ( subrelstr Lc) is complete LATTICE by YELLOW_2: 31;

      reconsider pc = (p | Lc) as Function of ( subrelstr Lc), ( subrelstr Lc) by A2, Th45;

      

       A5: ( Image pc) is infs-inheriting by A2, Th47, Th53;

      

       A6: the carrier of ( Image pc) = ( rng pc) by YELLOW_0:def 15

      .= the carrier of ( Image p) by A2, A1, Th44;

      

      then the InternalRel of ( Image pc) = (the InternalRel of ( subrelstr Lc) |_2 the carrier of ( Image p)) by YELLOW_0:def 14

      .= ((the InternalRel of L |_2 the carrier of ( subrelstr Lc)) |_2 the carrier of ( Image p)) by YELLOW_0:def 14

      .= (the InternalRel of L |_2 the carrier of ( Image p)) by A1, A3, WELLORD1: 22, XBOOLE_1: 17

      .= the InternalRel of ( Image p) by YELLOW_0:def 14;

      hence thesis by A4, A5, A6, YELLOW_2: 30;

    end;

    theorem :: WAYBEL_1:55

    for L be non empty Poset, c be Function of L, L st c is closure holds ( corestr c) is sups-preserving & for X be Subset of L st X c= the carrier of ( Image c) & ex_sup_of (X,L) holds ex_sup_of (X,( Image c)) & ( "\/" (X,( Image c))) = (c . ( "\/" (X,L)))

    proof

      let L be non empty Poset, c be Function of L, L;

      

       A1: ( corestr c) = c by Th30;

      assume

       A2: c is closure;

      then

       A3: c is idempotent by Def13;

       [( inclusion c), ( corestr c)] is Galois by A2, Th36;

      then

       A4: ( corestr c) is lower_adjoint;

      hence ( corestr c) is sups-preserving;

      let X be Subset of L such that

       A5: X c= the carrier of ( Image c) and

       A6: ex_sup_of (X,L);

      X c= ( rng c) by A5, YELLOW_0:def 15;

      then

       A7: (c .: X) = X by A3, YELLOW_2: 20;

      ( corestr c) preserves_sup_of X by A4, WAYBEL_0:def 33;

      hence thesis by A6, A1, A7;

    end;

    theorem :: WAYBEL_1:56

    for L be non empty Poset, k be Function of L, L st k is kernel holds ( corestr k) is infs-preserving & for X be Subset of L st X c= the carrier of ( Image k) & ex_inf_of (X,L) holds ex_inf_of (X,( Image k)) & ( "/\" (X,( Image k))) = (k . ( "/\" (X,L)))

    proof

      let L be non empty Poset, k be Function of L, L;

      

       A1: ( corestr k) = k by Th30;

      assume

       A2: k is kernel;

      then

       A3: k is idempotent by Def13;

       [( corestr k), ( inclusion k)] is Galois by A2, Th39;

      then

       A4: ( corestr k) is upper_adjoint;

      hence ( corestr k) is infs-preserving;

      let X be Subset of L such that

       A5: X c= the carrier of ( Image k) and

       A6: ex_inf_of (X,L);

      X c= ( rng k) by A5, YELLOW_0:def 15;

      then

       A7: (k .: X) = X by A3, YELLOW_2: 20;

      ( corestr k) preserves_inf_of X by A4, WAYBEL_0:def 32;

      hence thesis by A6, A1, A7;

    end;

    begin

    theorem :: WAYBEL_1:57

    

     Th57: for L be complete non empty Poset holds [( IdsMap L), ( SupMap L)] is Galois & ( SupMap L) is sups-preserving

    proof

      let L be complete non empty Poset;

      set g = ( IdsMap L), d = ( SupMap L);

      now

        let I be Element of ( InclPoset ( Ids L)), x be Element of L;

        reconsider I9 = I as Ideal of L by YELLOW_2: 41;

        hereby

          assume I <= (g . x);

          then I c= (g . x) by YELLOW_1: 3;

          then I9 c= ( downarrow x) by YELLOW_2:def 4;

          then x is_>=_than I9 by YELLOW_2: 1;

          then ( sup I9) <= x by YELLOW_0: 32;

          hence (d . I) <= x by YELLOW_2:def 3;

        end;

        assume (d . I) <= x;

        then

         A1: ( sup I9) <= x by YELLOW_2:def 3;

        ( sup I9) is_>=_than I9 by YELLOW_0: 32;

        then x is_>=_than I9 by A1, YELLOW_0: 4;

        then I9 c= ( downarrow x) by YELLOW_2: 1;

        then I c= (g . x) by YELLOW_2:def 4;

        hence I <= (g . x) by YELLOW_1: 3;

      end;

      hence [( IdsMap L), ( SupMap L)] is Galois;

      then ( SupMap L) is lower_adjoint;

      hence thesis;

    end;

    theorem :: WAYBEL_1:58

    for L be complete non empty Poset holds (( IdsMap L) * ( SupMap L)) is closure & (( Image (( IdsMap L) * ( SupMap L))),L) are_isomorphic

    proof

      let L be complete non empty Poset;

      set i = (( IdsMap L) * ( SupMap L));

       A1:

      now

        let I be Ideal of L;

        I is Element of ( InclPoset ( Ids L)) by YELLOW_2: 41;

        

        hence (i . I) = (( IdsMap L) . (( SupMap L) . I)) by FUNCT_2: 15

        .= (( IdsMap L) . ( sup I)) by YELLOW_2:def 3

        .= ( downarrow ( sup I)) by YELLOW_2:def 4;

      end;

      i is monotone & [( IdsMap L), ( SupMap L)] is Galois by Th57, YELLOW_2: 12;

      hence i is closure by Th38;

      take f = (( SupMap L) * ( inclusion i));

       A2:

      now

        let x be Element of ( Image i);

        let I be Ideal of L;

        assume

         A3: x = I;

        

        hence (f . I) = (( SupMap L) . (( inclusion i) . I)) by FUNCT_2: 15

        .= (( SupMap L) . I) by A3

        .= ( sup I) by YELLOW_2:def 3;

      end;

      

       A4: f is monotone by YELLOW_2: 12;

       A5:

      now

        let x,y be Element of ( Image i);

        consider Ix be Element of ( InclPoset ( Ids L)) such that

         A6: (i . Ix) = x by YELLOW_2: 10;

        thus x <= y implies (f . x) <= (f . y) by A4;

        assume

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

        x is Element of ( InclPoset ( Ids L)) & y is Element of ( InclPoset ( Ids L)) by YELLOW_0: 58;

        then

        reconsider x9 = x, y9 = y as Ideal of L by YELLOW_2: 41;

        consider Iy be Element of ( InclPoset ( Ids L)) such that

         A8: (i . Iy) = y by YELLOW_2: 10;

        reconsider Ix, Iy as Ideal of L by YELLOW_2: 41;

        reconsider i1 = ( downarrow ( sup Ix)), i2 = ( downarrow ( sup Iy)) as Element of ( InclPoset ( Ids L)) by YELLOW_2: 41;

        

         A9: (i . Ix) = ( downarrow ( sup Ix)) & (i . Iy) = ( downarrow ( sup Iy)) by A1;

        

         A10: (f . x9) = ( sup x9) & (f . y9) = ( sup y9) by A2;

        ( sup ( downarrow ( sup Ix))) = ( sup Ix) & ( sup ( downarrow ( sup Iy))) = ( sup Iy) by WAYBEL_0: 34;

        then ( downarrow ( sup Ix)) c= ( downarrow ( sup Iy)) by A7, A6, A8, A9, A10, WAYBEL_0: 21;

        then i1 <= i2 by YELLOW_1: 3;

        hence x <= y by A6, A8, A9, YELLOW_0: 60;

      end;

      

       A11: ( rng f) = the carrier of L

      proof

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

        let x be object;

        assume x in the carrier of L;

        then

        reconsider x as Element of L;

        

         A12: (( SupMap L) . ( downarrow x)) = ( sup ( downarrow x)) by YELLOW_2:def 3

        .= x by WAYBEL_0: 34;

        

         A13: ( downarrow x) is Element of ( InclPoset ( Ids L)) by YELLOW_2: 41;

        

        then (i . ( downarrow x)) = (( IdsMap L) . (( SupMap L) . ( downarrow x))) by FUNCT_2: 15

        .= ( downarrow x) by A12, YELLOW_2:def 4;

        then ( downarrow x) in ( rng i) by A13, FUNCT_2: 4;

        then

         A14: ( downarrow x) in the carrier of ( Image i) by YELLOW_0:def 15;

        

        then (f . ( downarrow x)) = (( SupMap L) . (( inclusion i) . ( downarrow x))) by FUNCT_2: 15

        .= (( SupMap L) . ( downarrow x)) by A14, FUNCT_1: 18;

        hence thesis by A12, A14, FUNCT_2: 4;

      end;

      f is one-to-one

      proof

        let x,y be Element of ( Image i);

        assume

         A15: (f . x) = (f . y);

        consider Ix be Element of ( InclPoset ( Ids L)) such that

         A16: (i . Ix) = x by YELLOW_2: 10;

        consider Iy be Element of ( InclPoset ( Ids L)) such that

         A17: (i . Iy) = y by YELLOW_2: 10;

        x is Element of ( InclPoset ( Ids L)) & y is Element of ( InclPoset ( Ids L)) by YELLOW_0: 58;

        then

        reconsider x, y as Ideal of L by YELLOW_2: 41;

        reconsider Ix, Iy as Ideal of L by YELLOW_2: 41;

        

         A18: ( sup ( downarrow ( sup Ix))) = ( sup Ix) by WAYBEL_0: 34;

        

         A19: (i . Ix) = ( downarrow ( sup Ix)) & (i . Iy) = ( downarrow ( sup Iy)) by A1;

        (f . x) = ( sup x) & (f . y) = ( sup y) by A2;

        hence thesis by A15, A16, A17, A19, A18, WAYBEL_0: 34;

      end;

      hence thesis by A11, A5, WAYBEL_0: 66;

    end;

    definition

      let S be non empty RelStr;

      let x be Element of S;

      :: WAYBEL_1:def18

      func x "/\" -> Function of S, S means

      : Def18: for s be Element of S holds (it . s) = (x "/\" s);

      existence

      proof

        deffunc F( Element of S) = (x "/\" $1);

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

      end;

      uniqueness

      proof

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

         A1: for s be Element of S holds (f1 . s) = (x "/\" s) and

         A2: for s be Element of S holds (f2 . s) = (x "/\" s);

        now

          let s be Element of S;

          

          thus (f1 . s) = (x "/\" s) by A1

          .= (f2 . s) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: WAYBEL_1:59

    

     Th59: for S be non empty RelStr, x,t be Element of S holds { s where s be Element of S : (x "/\" s) <= t } = ((x "/\" ) " ( downarrow t))

    proof

      let S be non empty RelStr, x,t be Element of S;

      hereby

        let a be object;

        assume a in { s where s be Element of S : (x "/\" s) <= t };

        then

        consider s be Element of S such that

         A1: a = s and

         A2: (x "/\" s) <= t;

        ((x "/\" ) . s) <= t by A2, Def18;

        then ((x "/\" ) . s) in ( downarrow t) by WAYBEL_0: 17;

        hence a in ((x "/\" ) " ( downarrow t)) by A1, FUNCT_2: 38;

      end;

      let s be object;

      assume

       A3: s in ((x "/\" ) " ( downarrow t));

      then

      reconsider s as Element of S;

      ((x "/\" ) . s) in ( downarrow t) by A3, FUNCT_2: 38;

      then (x "/\" s) in ( downarrow t) by Def18;

      then (x "/\" s) <= t by WAYBEL_0: 17;

      hence thesis;

    end;

    theorem :: WAYBEL_1:60

    

     Th60: for S be Semilattice, x be Element of S holds (x "/\" ) is monotone

    proof

      let S be Semilattice, x be Element of S;

      let s1,s2 be Element of S;

      assume

       A1: s1 <= s2;

      

       A2: ex_inf_of ( {x, s1},S) by YELLOW_0: 21;

      then

       A3: (x "/\" s1) <= x by YELLOW_0: 19;

      (x "/\" s1) <= s1 by A2, YELLOW_0: 19;

      then ex_inf_of ( {x, s2},S) & (x "/\" s1) <= s2 by A1, ORDERS_2: 3, YELLOW_0: 21;

      then (x "/\" s1) <= (x "/\" s2) by A3, YELLOW_0: 19;

      then ((x "/\" ) . s1) <= (x "/\" s2) by Def18;

      hence ((x "/\" ) . s1) <= ((x "/\" ) . s2) by Def18;

    end;

    registration

      let S be Semilattice, x be Element of S;

      cluster (x "/\" ) -> monotone;

      coherence by Th60;

    end

    theorem :: WAYBEL_1:61

    

     Th61: for S be non empty RelStr, x be Element of S, X be Subset of S holds ((x "/\" ) .: X) = { (x "/\" y) where y be Element of S : y in X }

    proof

      let S be non empty RelStr, x be Element of S, X be Subset of S;

      set Y = { (x "/\" y) where y be Element of S : y in X };

      hereby

        let y be object;

        assume y in ((x "/\" ) .: X);

        then

        consider z be object such that

         A1: z in the carrier of S and

         A2: z in X and

         A3: y = ((x "/\" ) . z) by FUNCT_2: 64;

        reconsider z as Element of S by A1;

        y = (x "/\" z) by A3, Def18;

        hence y in Y by A2;

      end;

      let y be object;

      assume y in Y;

      then

      consider z be Element of S such that

       A4: y = (x "/\" z) and

       A5: z in X;

      y = ((x "/\" ) . z) by A4, Def18;

      hence thesis by A5, FUNCT_2: 35;

    end;

    theorem :: WAYBEL_1:62

    

     Th62: for S be Semilattice holds (for x be Element of S holds (x "/\" ) is lower_adjoint) iff for x,t be Element of S holds ex_max_of ({ s where s be Element of S : (x "/\" s) <= t },S)

    proof

      let S be Semilattice;

      hereby

        assume

         A1: for x be Element of S holds (x "/\" ) is lower_adjoint;

        let x,t be Element of S;

        (x "/\" ) is lower_adjoint by A1;

        then

        consider g be Function of S, S such that

         A2: [g, (x "/\" )] is Galois;

        set X = { s where s be Element of S : (x "/\" s) <= t };

        

         A3: X = ((x "/\" ) " ( downarrow t)) by Th59;

        (g . t) is_maximum_of ((x "/\" ) " ( downarrow t)) by A2, Th11;

        then ex_sup_of (X,S) & ( "\/" (X,S)) in X by A3;

        hence ex_max_of (X,S);

      end;

      assume

       A4: for x,t be Element of S holds ex_max_of ({ s where s be Element of S : (x "/\" s) <= t },S);

      let x be Element of S;

      deffunc F( Element of S) = ( "\/" (((x "/\" ) " ( downarrow $1)),S));

      consider g be Function of S, S such that

       A5: for s be Element of S holds (g . s) = F(s) from FUNCT_2:sch 4;

      now

        let t be Element of S;

        set X = { s where s be Element of S : (x "/\" s) <= t };

         ex_max_of (X,S) by A4;

        then

         A6: ex_sup_of (X,S) & ( "\/" (X,S)) in X;

        X = ((x "/\" ) " ( downarrow t)) & (g . t) = ( "\/" (((x "/\" ) " ( downarrow t)),S)) by A5, Th59;

        hence (g . t) is_maximum_of ((x "/\" ) " ( downarrow t)) by A6;

      end;

      then [g, (x "/\" )] is Galois by Th11;

      hence thesis;

    end;

    theorem :: WAYBEL_1:63

    

     Th63: for S be Semilattice st for x be Element of S holds (x "/\" ) is lower_adjoint holds for X be Subset of S st ex_sup_of (X,S) holds for x be Element of S holds (x "/\" ( "\/" (X,S))) = ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S))

    proof

      let S be Semilattice such that

       A1: for x be Element of S holds (x "/\" ) is lower_adjoint;

      let X be Subset of S such that

       A2: ex_sup_of (X,S);

      let x be Element of S;

      (x "/\" ) is sups-preserving by A1, Th13;

      then (x "/\" ) preserves_sup_of X;

      then ( sup ((x "/\" ) .: X)) = ((x "/\" ) . ( sup X)) by A2;

      

      hence (x "/\" ( "\/" (X,S))) = ( sup ((x "/\" ) .: X)) by Def18

      .= ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S)) by Th61;

    end;

    theorem :: WAYBEL_1:64

    for S be complete non empty Poset holds (for x be Element of S holds (x "/\" ) is lower_adjoint) iff for X be Subset of S, x be Element of S holds (x "/\" ( "\/" (X,S))) = ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S))

    proof

      let S be complete non empty Poset;

      thus (for x be Element of S holds (x "/\" ) is lower_adjoint) implies for X be Subset of S, x be Element of S holds (x "/\" ( "\/" (X,S))) = ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S)) by Th63, YELLOW_0: 17;

      assume

       A1: for X be Subset of S, x be Element of S holds (x "/\" ( "\/" (X,S))) = ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S));

      let x be Element of S;

      (x "/\" ) is sups-preserving

      proof

        let X be Subset of S;

        assume ex_sup_of (X,S);

        thus ex_sup_of (((x "/\" ) .: X),S) by YELLOW_0: 17;

        

        thus ((x "/\" ) . ( sup X)) = (x "/\" ( "\/" (X,S))) by Def18

        .= ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S)) by A1

        .= ( sup ((x "/\" ) .: X)) by Th61;

      end;

      hence thesis by Th17;

    end;

    theorem :: WAYBEL_1:65

    

     Th65: for S be LATTICE st for X be Subset of S st ex_sup_of (X,S) holds for x be Element of S holds (x "/\" ( "\/" (X,S))) = ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S)) holds S is distributive

    proof

      let S be LATTICE such that

       A1: for X be Subset of S st ex_sup_of (X,S) holds for x be Element of S holds (x "/\" ( "\/" (X,S))) = ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S));

      let x,y,z be Element of S;

      set Y = { (x "/\" s) where s be Element of S : s in {y, z} };

      

       A2: ex_sup_of ( {y, z},S) by YELLOW_0: 20;

      now

        let t be object;

        hereby

          assume t in Y;

          then ex s be Element of S st t = (x "/\" s) & s in {y, z};

          hence t = (x "/\" y) or t = (x "/\" z) by TARSKI:def 2;

        end;

        assume

         A3: t = (x "/\" y) or t = (x "/\" z);

        per cases by A3;

          suppose

           A4: t = (x "/\" y);

          y in {y, z} by TARSKI:def 2;

          hence t in Y by A4;

        end;

          suppose

           A5: t = (x "/\" z);

          z in {y, z} by TARSKI:def 2;

          hence t in Y by A5;

        end;

      end;

      then

       A6: Y = {(x "/\" y), (x "/\" z)} by TARSKI:def 2;

      

      thus (x "/\" (y "\/" z)) = (x "/\" ( sup {y, z})) by YELLOW_0: 41

      .= ( "\/" ( {(x "/\" y), (x "/\" z)},S)) by A1, A6, A2

      .= ((x "/\" y) "\/" (x "/\" z)) by YELLOW_0: 41;

    end;

    definition

      let H be non empty RelStr;

      :: WAYBEL_1:def19

      attr H is Heyting means H is LATTICE & for x be Element of H holds (x "/\" ) is lower_adjoint;

    end

    registration

      cluster Heyting -> with_infima with_suprema reflexive transitive antisymmetric for non empty RelStr;

      coherence ;

    end

    definition

      let H be non empty RelStr, a be Element of H;

      assume

       A1: H is Heyting;

      :: WAYBEL_1:def20

      func a => -> Function of H, H means

      : Def20: [it , (a "/\" )] is Galois;

      existence by A1, Def12;

      uniqueness

      proof

        let g1,g2 be Function of H, H such that

         A2: [g1, (a "/\" )] is Galois and

         A3: [g2, (a "/\" )] is Galois;

        now

          let x be Element of H;

          (g1 . x) is_maximum_of ((a "/\" ) " ( downarrow x)) by A1, A2, Th11;

          then

           A4: (g1 . x) = ( "\/" (((a "/\" ) " ( downarrow x)),H));

          (g2 . x) is_maximum_of ((a "/\" ) " ( downarrow x)) by A1, A3, Th11;

          hence (g1 . x) = (g2 . x) by A4;

        end;

        hence g1 = g2 by FUNCT_2: 63;

      end;

    end

    theorem :: WAYBEL_1:66

    

     Th66: for H be non empty RelStr st H is Heyting holds H is distributive

    proof

      let H be non empty RelStr;

      assume that

       A1: H is LATTICE and

       A2: for x be Element of H holds (x "/\" ) is lower_adjoint;

      for X be Subset of H st ex_sup_of (X,H) holds for x be Element of H holds (x "/\" ( "\/" (X,H))) = ( "\/" ({ (x "/\" y) where y be Element of H : y in X },H)) by A1, A2, Th63;

      hence thesis by A1, Th65;

    end;

    registration

      cluster Heyting -> distributive for non empty RelStr;

      coherence by Th66;

    end

    definition

      let H be non empty RelStr, a,y be Element of H;

      :: WAYBEL_1:def21

      func a => y -> Element of H equals ((a => ) . y);

      correctness ;

    end

    theorem :: WAYBEL_1:67

    

     Th67: for H be non empty RelStr st H is Heyting holds for x,a,y be Element of H holds x >= (a "/\" y) iff (a => x) >= y

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let x,a,y be Element of H;

       [(a => ), (a "/\" )] is Galois by A1, Def20;

      then x >= ((a "/\" ) . y) iff ((a => ) . x) >= y by A1, Th8;

      hence thesis by Def18;

    end;

    theorem :: WAYBEL_1:68

    

     Th68: for H be non empty RelStr st H is Heyting holds H is upper-bounded

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      set a = the Element of H;

      take (a => a);

      let y be Element of H;

      assume y in the carrier of H;

      a >= (a "/\" y) by A1, YELLOW_0: 23;

      hence thesis by A1, Th67;

    end;

    registration

      cluster Heyting -> upper-bounded for non empty RelStr;

      coherence by Th68;

    end

    theorem :: WAYBEL_1:69

    

     Th69: for H be non empty RelStr st H is Heyting holds for a,b be Element of H holds ( Top H) = (a => b) iff a <= b

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a,b be Element of H;

      

       A2: (a "/\" ( Top H)) = (( Top H) "/\" a) by A1, LATTICE3: 15

      .= a by A1, Th4;

      hereby

        assume ( Top H) = (a => b);

        then (a => b) >= ( Top H) by A1, ORDERS_2: 1;

        hence a <= b by A1, A2, Th67;

      end;

      assume a <= b;

      then

       A3: (a => b) >= ( Top H) by A1, A2, Th67;

      (a => b) <= ( Top H) by A1, YELLOW_0: 45;

      hence thesis by A1, A3, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_1:70

    for H be non empty RelStr st H is Heyting holds for a be Element of H holds ( Top H) = (a => a)

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a be Element of H;

      a >= (a "/\" ( Top H)) by A1, YELLOW_0: 23;

      then

       A2: ( Top H) <= (a => a) by A1, Th67;

      ( Top H) >= (a => a) by A1, YELLOW_0: 45;

      hence thesis by A1, A2, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_1:71

    for H be non empty RelStr st H is Heyting holds for a,b be Element of H st ( Top H) = (a => b) & ( Top H) = (b => a) holds a = b

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a,b be Element of H;

      assume

       A2: ( Top H) = (a => b);

      assume ( Top H) = (b => a);

      then

       A3: b <= a by A1, Th69;

      a <= b by A1, A2, Th69;

      hence thesis by A1, A3, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_1:72

    

     Th72: for H be non empty RelStr st H is Heyting holds for a,b be Element of H holds b <= (a => b)

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a,b be Element of H;

      (a "/\" b) <= b by A1, YELLOW_0: 23;

      hence thesis by A1, Th67;

    end;

    theorem :: WAYBEL_1:73

    for H be non empty RelStr st H is Heyting holds for a be Element of H holds ( Top H) = (a => ( Top H))

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a be Element of H;

      a <= ( Top H) by A1, YELLOW_0: 45;

      hence thesis by A1, Th69;

    end;

    theorem :: WAYBEL_1:74

    for H be non empty RelStr st H is Heyting holds for b be Element of H holds b = (( Top H) => b)

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let b be Element of H;

      (( Top H) => b) <= (( Top H) => b) by A1, ORDERS_2: 1;

      then (( Top H) "/\" (( Top H) => b)) <= b by A1, Th67;

      then

       A2: (( Top H) => b) <= b by A1, Th4;

      (( Top H) => b) >= b by A1, Th72;

      hence thesis by A1, A2, ORDERS_2: 2;

    end;

    

     Lm5: for H be non empty RelStr st H is Heyting holds for a,b be Element of H holds (a "/\" (a => b)) <= b

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a,b be Element of H;

      (a => b) <= (a => b) by A1, ORDERS_2: 1;

      hence thesis by A1, Th67;

    end;

    theorem :: WAYBEL_1:75

    

     Th75: for H be non empty RelStr st H is Heyting holds for a,b,c be Element of H st a <= b holds (b => c) <= (a => c)

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a,b,c be Element of H;

      assume a <= b;

      then

       A2: (a "/\" (b => c)) <= (b "/\" (b => c)) by A1, Th1;

      (b "/\" (b => c)) <= c by A1, Lm5;

      then (a "/\" (b => c)) <= c by A1, A2, ORDERS_2: 3;

      hence thesis by A1, Th67;

    end;

    theorem :: WAYBEL_1:76

    for H be non empty RelStr st H is Heyting holds for a,b,c be Element of H st b <= c holds (a => b) <= (a => c)

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a,b,c be Element of H;

      assume

       A2: b <= c;

      (a "/\" (a => b)) <= b by A1, Lm5;

      then (a "/\" (a => b)) <= c by A1, A2, ORDERS_2: 3;

      hence thesis by A1, Th67;

    end;

    theorem :: WAYBEL_1:77

    

     Th77: for H be non empty RelStr st H is Heyting holds for a,b be Element of H holds (a "/\" (a => b)) = (a "/\" b)

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a,b be Element of H;

      ((a "/\" (a => b)) "/\" a) <= (b "/\" a) by A1, Lm5, Th1;

      then (a "/\" (a "/\" (a => b))) <= (b "/\" a) by A1, LATTICE3: 15;

      then (a "/\" (a "/\" (a => b))) <= (a "/\" b) by A1, LATTICE3: 15;

      then ((a "/\" a) "/\" (a => b)) <= (a "/\" b) by A1, LATTICE3: 16;

      then

       A2: (a "/\" (a => b)) <= (a "/\" b) by A1, YELLOW_0: 25;

      (b "/\" a) <= ((a => b) "/\" a) by A1, Th1, Th72;

      then (a "/\" b) <= ((a => b) "/\" a) by A1, LATTICE3: 15;

      then (a "/\" b) <= (a "/\" (a => b)) by A1, LATTICE3: 15;

      hence thesis by A1, A2, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_1:78

    

     Th78: for H be non empty RelStr st H is Heyting holds for a,b,c be Element of H holds ((a "\/" b) => c) = ((a => c) "/\" (b => c))

    proof

      let H be non empty RelStr;

      assume

       A1: H is Heyting;

      let a,b,c be Element of H;

      ((a "/\" c) "/\" (b => c)) <= (a "/\" c) & (a "/\" c) <= c by A1, YELLOW_0: 23;

      then

       A2: ((a "/\" c) "/\" (b => c)) <= c by A1, ORDERS_2: 3;

      ((b "/\" c) "/\" (a => c)) <= (b "/\" c) & (b "/\" c) <= c by A1, YELLOW_0: 23;

      then

       A3: ((b "/\" c) "/\" (a => c)) <= c by A1, ORDERS_2: 3;

      set d = ((a => c) "/\" (b => c));

      ((a "\/" b) "/\" d) = (d "/\" (a "\/" b)) by A1, LATTICE3: 15

      .= ((d "/\" a) "\/" (d "/\" b)) by A1, Def3

      .= ((a "/\" d) "\/" (d "/\" b)) by A1, LATTICE3: 15

      .= ((a "/\" d) "\/" (b "/\" d)) by A1, LATTICE3: 15

      .= (((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" d)) by A1, LATTICE3: 16

      .= (((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((b => c) "/\" (a => c)))) by A1, LATTICE3: 15

      .= (((a "/\" (a => c)) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c))) by A1, LATTICE3: 16

      .= (((a "/\" c) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c))) by A1, Th77

      .= (((a "/\" c) "/\" (b => c)) "\/" ((b "/\" c) "/\" (a => c))) by A1, Th77;

      then ((a "\/" b) "/\" d) <= c by A1, A2, A3, YELLOW_0: 22;

      then

       A4: ((a "\/" b) => c) >= d by A1, Th67;

      b <= (a "\/" b) by A1, YELLOW_0: 22;

      then

       A5: ((a "\/" b) => c) <= (b => c) by A1, Th75;

      a <= (a "\/" b) by A1, YELLOW_0: 22;

      then ((a "\/" b) => c) <= (a => c) by A1, Th75;

      then ((a "\/" b) => c) <= ((a => c) "/\" (b => c)) by A1, A5, YELLOW_0: 23;

      hence thesis by A1, A4, ORDERS_2: 2;

    end;

    definition

      let H be non empty RelStr, a be Element of H;

      :: WAYBEL_1:def22

      func 'not' a -> Element of H equals (a => ( Bottom H));

      correctness ;

    end

    theorem :: WAYBEL_1:79

    for H be non empty RelStr st H is Heyting & H is lower-bounded holds for a be Element of H holds ( 'not' a) is_maximum_of { x where x be Element of H : (a "/\" x) = ( Bottom H) }

    proof

      let H be non empty RelStr such that

       A1: H is Heyting and

       A2: H is lower-bounded;

      let a be Element of H;

      set X = { x where x be Element of H : (a "/\" x) = ( Bottom H) }, Y = { x where x be Element of H : (a "/\" x) <= ( Bottom H) };

      

       A3: X = Y

      proof

        hereby

          let y be object;

          assume y in X;

          then

          consider x be Element of H such that

           A4: y = x and

           A5: (a "/\" x) = ( Bottom H);

          (a "/\" x) <= ( Bottom H) by A1, A5, ORDERS_2: 1;

          hence y in Y by A4;

        end;

        let y be object;

        assume y in Y;

        then

        consider x be Element of H such that

         A6: y = x and

         A7: (a "/\" x) <= ( Bottom H);

        ( Bottom H) <= (a "/\" x) by A1, A2, YELLOW_0: 44;

        then ( Bottom H) = (a "/\" x) by A1, A7, ORDERS_2: 2;

        hence thesis by A6;

      end;

       A8:

      now

        (a => ( Bottom H)) <= (a => ( Bottom H)) by A1, ORDERS_2: 1;

        then (a "/\" ( 'not' a)) <= ( Bottom H) by A1, Th67;

        then

         A9: ( 'not' a) in X by A3;

        let b be Element of H;

        assume b is_>=_than X;

        hence ( 'not' a) <= b by A9;

      end;

      

       A10: ex_max_of (X,H) by A1, A3, Th62;

      hence ex_sup_of (X,H);

      ( 'not' a) is_>=_than X

      proof

        let b be Element of H;

        assume b in X;

        then ex x be Element of H st x = b & (a "/\" x) <= ( Bottom H) by A3;

        hence thesis by A1, Th67;

      end;

      hence ( 'not' a) = ( "\/" (X,H)) by A1, A8, YELLOW_0: 30;

      thus thesis by A10;

    end;

    theorem :: WAYBEL_1:80

    

     Th80: for H be non empty RelStr st H is Heyting & H is lower-bounded holds ( 'not' ( Bottom H)) = ( Top H) & ( 'not' ( Top H)) = ( Bottom H)

    proof

      let H be non empty RelStr such that

       A1: H is Heyting and

       A2: H is lower-bounded;

      (( Top H) => ( Bottom H)) <= (( Top H) => ( Bottom H)) by A1, ORDERS_2: 1;

      then

       A3: ( Bottom H) >= (( Top H) "/\" ( 'not' ( Top H))) by A1, Th67;

      ( Bottom H) >= (( Bottom H) "/\" ( Top H)) by A1, YELLOW_0: 23;

      then

       A4: ( Top H) <= (( Bottom H) => ( Bottom H)) by A1, Th67;

      ( Bottom H) <= (( Top H) "/\" ( 'not' ( Top H))) by A1, A2, YELLOW_0: 44;

      then

       A5: ( Bottom H) = (( Top H) "/\" ( 'not' ( Top H))) by A1, A3, ORDERS_2: 2;

      ( 'not' ( Bottom H)) <= ( Top H) by A1, YELLOW_0: 45;

      hence ( Top H) = ( 'not' ( Bottom H)) by A1, A4, ORDERS_2: 2;

      ( 'not' ( Top H)) <= ( Top H) by A1, YELLOW_0: 45;

      

      hence ( 'not' ( Top H)) = (( 'not' ( Top H)) "/\" ( Top H)) by A1, YELLOW_0: 25

      .= ( Bottom H) by A1, A5, LATTICE3: 15;

    end;

    theorem :: WAYBEL_1:81

    for H be non empty lower-bounded RelStr st H is Heyting holds for a,b be Element of H holds ( 'not' a) >= b iff ( 'not' b) >= a

    proof

      let H be non empty lower-bounded RelStr such that

       A1: H is Heyting;

      let a,b be Element of H;

      

       A2: ( Bottom H) >= (a "/\" b) iff (a => ( Bottom H)) >= b by A1, Th67;

      ( Bottom H) >= (b "/\" a) iff (b => ( Bottom H)) >= a by A1, Th67;

      hence thesis by A1, A2, LATTICE3: 15;

    end;

    theorem :: WAYBEL_1:82

    

     Th82: for H be non empty lower-bounded RelStr st H is Heyting holds for a,b be Element of H holds ( 'not' a) >= b iff (a "/\" b) = ( Bottom H)

    proof

      let H be non empty lower-bounded RelStr;

      assume

       A1: H is Heyting;

      let a,b be Element of H;

      hereby

        assume ( 'not' a) >= b;

        then

         A2: (a "/\" b) <= ( Bottom H) by A1, Th67;

        (a "/\" b) >= ( Bottom H) by A1, YELLOW_0: 44;

        hence (a "/\" b) = ( Bottom H) by A1, A2, ORDERS_2: 2;

      end;

      assume (a "/\" b) = ( Bottom H);

      then (a "/\" b) <= ( Bottom H) by A1, ORDERS_2: 1;

      hence thesis by A1, Th67;

    end;

    theorem :: WAYBEL_1:83

    for H be non empty lower-bounded RelStr st H is Heyting holds for a,b be Element of H st a <= b holds ( 'not' b) <= ( 'not' a)

    proof

      let H be non empty lower-bounded RelStr such that

       A1: H is Heyting;

      let a,b be Element of H;

      

       A2: ( 'not' b) >= ( 'not' b) by A1, ORDERS_2: 1;

      assume a <= b;

      

      then (a "/\" ( 'not' b)) = ((a "/\" b) "/\" ( 'not' b)) by A1, YELLOW_0: 25

      .= (a "/\" (b "/\" ( 'not' b))) by A1, LATTICE3: 16

      .= (a "/\" ( Bottom H)) by A1, A2, Th82

      .= (( Bottom H) "/\" a) by A1, LATTICE3: 15

      .= ( Bottom H) by A1, Th3;

      hence thesis by A1, Th82;

    end;

    theorem :: WAYBEL_1:84

    for H be non empty lower-bounded RelStr st H is Heyting holds for a,b be Element of H holds ( 'not' (a "\/" b)) = (( 'not' a) "/\" ( 'not' b)) by Th78;

    theorem :: WAYBEL_1:85

    for H be non empty lower-bounded RelStr st H is Heyting holds for a,b be Element of H holds ( 'not' (a "/\" b)) >= (( 'not' a) "\/" ( 'not' b))

    proof

      let H be non empty lower-bounded RelStr;

      assume

       A1: H is Heyting;

      then

       A2: ( Bottom H) <= ( Bottom H) by ORDERS_2: 1;

      let a,b be Element of H;

      

       A3: ( 'not' a) <= ( 'not' a) by A1, ORDERS_2: 1;

      

       A4: ( 'not' b) <= ( 'not' b) by A1, ORDERS_2: 1;

      ((a "/\" b) "/\" (( 'not' a) "\/" ( 'not' b))) = (((a "/\" b) "/\" ( 'not' a)) "\/" ((a "/\" b) "/\" ( 'not' b))) by A1, Def3

      .= (((b "/\" a) "/\" ( 'not' a)) "\/" ((a "/\" b) "/\" ( 'not' b))) by A1, LATTICE3: 15

      .= ((b "/\" (a "/\" ( 'not' a))) "\/" ((a "/\" b) "/\" ( 'not' b))) by A1, LATTICE3: 16

      .= ((b "/\" (a "/\" ( 'not' a))) "\/" (a "/\" (b "/\" ( 'not' b)))) by A1, LATTICE3: 16

      .= ((b "/\" ( Bottom H)) "\/" (a "/\" (b "/\" ( 'not' b)))) by A1, A3, Th82

      .= ((b "/\" ( Bottom H)) "\/" (a "/\" ( Bottom H))) by A1, A4, Th82

      .= ((( Bottom H) "/\" b) "\/" (a "/\" ( Bottom H))) by A1, LATTICE3: 15

      .= ((( Bottom H) "/\" b) "\/" (( Bottom H) "/\" a)) by A1, LATTICE3: 15

      .= (( Bottom H) "\/" (( Bottom H) "/\" a)) by A1, Th3

      .= (( Bottom H) "\/" ( Bottom H)) by A1, Th3

      .= ( Bottom H) by A1, A2, YELLOW_0: 24;

      hence thesis by A1, Th82;

    end;

    definition

      let L be non empty RelStr, x,y be Element of L;

      :: WAYBEL_1:def23

      pred y is_a_complement_of x means (x "\/" y) = ( Top L) & (x "/\" y) = ( Bottom L);

    end

    definition

      let L be non empty RelStr;

      :: WAYBEL_1:def24

      attr L is complemented means for x be Element of L holds ex y be Element of L st y is_a_complement_of x;

    end

    registration

      let X be set;

      cluster ( BoolePoset X) -> complemented;

      coherence

      proof

        let x be Element of ( BoolePoset X);

        

         A1: the carrier of ( BoolePoset X) = the carrier of ( LattPOSet ( BooleLatt X)) by YELLOW_1:def 2

        .= ( bool X) by LATTICE3:def 1;

        then

        reconsider y = (X \ x) as Element of ( BoolePoset X) by XBOOLE_1: 109;

        take y;

        

        thus (x "\/" y) = (x \/ y) by YELLOW_1: 17

        .= (X \/ x) by XBOOLE_1: 39

        .= X by A1, XBOOLE_1: 12

        .= ( Top ( BoolePoset X)) by YELLOW_1: 19;

        

         A2: x misses y by XBOOLE_1: 79;

        

        thus (x "/\" y) = (x /\ y) by YELLOW_1: 17

        .= {} by A2

        .= ( Bottom ( BoolePoset X)) by YELLOW_1: 18;

      end;

    end

    

     Lm6: for L be bounded LATTICE st L is distributive complemented holds for x be Element of L holds ex x9 be Element of L st for y be Element of L holds ((y "\/" x9) "/\" x) <= y & y <= ((y "/\" x) "\/" x9)

    proof

      let L be bounded LATTICE such that

       A1: L is distributive and

       A2: L is complemented;

      let x be Element of L;

      consider x9 be Element of L such that

       A3: x9 is_a_complement_of x by A2;

      take x9;

      let y be Element of L;

      ((y "\/" x9) "/\" x) = ((x "/\" y) "\/" (x "/\" x9)) by A1

      .= (( Bottom L) "\/" (x "/\" y)) by A3

      .= (x "/\" y) by Th3;

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

      ((y "/\" x) "\/" x9) = ((x9 "\/" y) "/\" (x9 "\/" x)) by A1, Th5

      .= ((x9 "\/" y) "/\" ( Top L)) by A3

      .= (x9 "\/" y) by Th4;

      hence thesis by YELLOW_0: 22;

    end;

    

     Lm7: for L be bounded LATTICE st for x be Element of L holds ex x9 be Element of L st for y be Element of L holds ((y "\/" x9) "/\" x) <= y & y <= ((y "/\" x) "\/" x9) holds L is Heyting & for x be Element of L holds ( 'not' ( 'not' x)) = x

    proof

      let L be bounded LATTICE;

      defpred P[ Element of L, Element of L] means for y be Element of L holds ((y "\/" $2) "/\" $1) <= y & y <= ((y "/\" $1) "\/" $2);

      assume

       A1: for x be Element of L holds ex x9 be Element of L st P[x, x9];

      consider g9 be Function of L, L such that

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

       A3:

      now

        let y be Element of L;

        let g be Function of L, L such that

         A4: for z be Element of L holds (g . z) = ((g9 . y) "\/" z);

         A5:

        now

          let x be Element of L, z be Element of L;

          hereby

            assume x <= (g . z);

            then x <= ((g9 . y) "\/" z) by A4;

            then

             A6: (x "/\" y) <= (((g9 . y) "\/" z) "/\" y) by Th1;

            (((g9 . y) "\/" z) "/\" y) <= z by A2;

            then (x "/\" y) <= z by A6, ORDERS_2: 3;

            hence ((y "/\" ) . x) <= z by Def18;

          end;

          assume ((y "/\" ) . x) <= z;

          then (y "/\" x) <= z by Def18;

          then

           A7: ((x "/\" y) "\/" (g9 . y)) <= (z "\/" (g9 . y)) by Th2;

          x <= ((x "/\" y) "\/" (g9 . y)) by A2;

          then x <= (z "\/" (g9 . y)) by A7, ORDERS_2: 3;

          hence x <= (g . z) by A4;

        end;

        g is monotone

        proof

          let z1,z2 be Element of L;

          assume z1 <= z2;

          then ((g9 . y) "\/" z1) <= (z2 "\/" (g9 . y)) by Th2;

          then (g . z1) <= ((g9 . y) "\/" z2) by A4;

          hence thesis by A4;

        end;

        hence [g, (y "/\" )] is Galois by A5;

      end;

      thus

       A8: L is Heyting

      proof

        thus L is LATTICE;

        let y be Element of L;

        deffunc F( Element of L) = ((g9 . y) "\/" $1);

        consider g be Function of L, L such that

         A9: for z be Element of L holds (g . z) = F(z) from FUNCT_2:sch 4;

         [g, (y "/\" )] is Galois by A3, A9;

        hence thesis;

      end;

       A10:

      now

        let x be Element of L;

        deffunc F( Element of L) = ((g9 . x) "\/" $1);

        consider g be Function of L, L such that

         A11: for z be Element of L holds (g . z) = F(z) from FUNCT_2:sch 4;

         [g, (x "/\" )] is Galois by A3, A11;

        then g = (x => ) by A8, Def20;

        

        hence ( 'not' x) = (( Bottom L) "\/" (g9 . x)) by A11

        .= (g9 . x) by Th3;

      end;

       A12:

      now

        let x be Element of L;

        ((( Bottom L) "\/" (g9 . x)) "/\" x) <= ( Bottom L) by A2;

        then ((x "/\" ( Bottom L)) "\/" (x "/\" (g9 . x))) <= ( Bottom L) by A8, Def3;

        then (( Bottom L) "\/" (x "/\" (g9 . x))) <= ( Bottom L) by Th3;

        then

         A13: (x "/\" (g9 . x)) <= ( Bottom L) by Th3;

        ( Bottom L) <= (x "/\" (g9 . x)) by YELLOW_0: 44;

        

        hence ( Bottom L) = (x "/\" (g9 . x)) by A13, ORDERS_2: 2

        .= (x "/\" ( 'not' x)) by A10;

      end;

      let x be Element of L;

       A14:

      now

        let x be Element of L;

        ( Top L) <= ((( Top L) "/\" x) "\/" (g9 . x)) by A2;

        then

         A15: ( Top L) <= (x "\/" (g9 . x)) by Th4;

        (x "\/" (g9 . x)) <= ( Top L) by YELLOW_0: 45;

        

        hence ( Top L) = (x "\/" (g9 . x)) by A15, ORDERS_2: 2

        .= (x "\/" ( 'not' x)) by A10;

      end;

      then ((( 'not' x) "\/" ( 'not' ( 'not' x))) "/\" x) = (( Top L) "/\" x);

      

      then x = (x "/\" (( 'not' x) "\/" ( 'not' ( 'not' x)))) by Th4

      .= ((x "/\" ( 'not' x)) "\/" (x "/\" ( 'not' ( 'not' x)))) by A8, Def3

      .= (( Bottom L) "\/" (x "/\" ( 'not' ( 'not' x)))) by A12

      .= (x "/\" ( 'not' ( 'not' x))) by Th3;

      then

       A16: x <= ( 'not' ( 'not' x)) by YELLOW_0: 25;

      (( Bottom L) "\/" x) = ((( 'not' x) "/\" ( 'not' ( 'not' x))) "\/" x) by A12;

      

      then x = (x "\/" (( 'not' x) "/\" ( 'not' ( 'not' x)))) by Th3

      .= ((x "\/" ( 'not' x)) "/\" (x "\/" ( 'not' ( 'not' x)))) by A8, Th5

      .= (( Top L) "/\" (x "\/" ( 'not' ( 'not' x)))) by A14

      .= (x "\/" ( 'not' ( 'not' x))) by Th4;

      hence thesis by A16, YELLOW_0: 24;

    end;

    theorem :: WAYBEL_1:86

    

     Th86: for L be bounded LATTICE st L is Heyting & for x be Element of L holds ( 'not' ( 'not' x)) = x holds for x be Element of L holds ( 'not' x) is_a_complement_of x

    proof

      let L be bounded LATTICE such that

       A1: L is Heyting and

       A2: for x be Element of L holds ( 'not' ( 'not' x)) = x;

      let x be Element of L;

      

       A3: ( 'not' (x "\/" ( 'not' x))) = (( 'not' x) "/\" ( 'not' ( 'not' x))) by A1, Th78

      .= (x "/\" ( 'not' x)) by A2;

      

       A4: ( 'not' x) >= ( 'not' x) by ORDERS_2: 1;

      then (x "/\" ( 'not' x)) = ( Bottom L) by A1, Th82;

      

      hence (x "\/" ( 'not' x)) = ( 'not' ( Bottom L)) by A2, A3

      .= ( Top L) by A1, Th80;

      thus thesis by A1, A4, Th82;

    end;

    theorem :: WAYBEL_1:87

    

     Th87: for L be bounded LATTICE holds L is distributive complemented iff L is Heyting & for x be Element of L holds ( 'not' ( 'not' x)) = x

    proof

      let L be bounded LATTICE;

      hereby

        assume L is distributive complemented;

        then for x be Element of L holds ex x9 be Element of L st for y be Element of L holds ((y "\/" x9) "/\" x) <= y & y <= ((y "/\" x) "\/" x9) by Lm6;

        hence L is Heyting & for x be Element of L holds ( 'not' ( 'not' x)) = x by Lm7;

      end;

      assume that

       A1: L is Heyting and

       A2: for x be Element of L holds ( 'not' ( 'not' x)) = x;

      thus L is distributive by A1;

      let x be Element of L;

      take ( 'not' x);

      thus thesis by A1, A2, Th86;

    end;

    definition

      let B be non empty RelStr;

      :: WAYBEL_1:def25

      attr B is Boolean means B is LATTICE & B is bounded distributive complemented;

    end

    registration

      cluster Boolean -> reflexive transitive antisymmetric with_infima with_suprema bounded distributive complemented for non empty RelStr;

      coherence ;

    end

    registration

      cluster reflexive transitive antisymmetric with_infima with_suprema bounded distributive complemented -> Boolean for non empty RelStr;

      coherence ;

    end

    registration

      cluster Boolean -> Heyting for non empty RelStr;

      coherence by Th87;

    end

    registration

      cluster strict Boolean non empty for LATTICE;

      existence

      proof

        take ( BoolePoset {} );

        thus thesis;

      end;

    end

    registration

      cluster strict Heyting non empty for LATTICE;

      existence

      proof

        set L = the strict Boolean non empty LATTICE;

        take L;

        thus thesis;

      end;

    end