quantal1.miz

    begin

    scheme :: QUANTAL1:sch1

    DenestFraenkel { A() -> non empty set , B() -> non empty set , F( set) -> set , G( set) -> Element of B() , P[ set] } :

{ F(a) where a be Element of B() : a in { G(b) where b be Element of A() : P[b] } } = { F(G) where a be Element of A() : P[a] };

      thus { F(a) where a be Element of B() : a in { G(b) where b be Element of A() : P[b] } } c= { F(G) where a be Element of A() : P[a] }

      proof

        let x be object;

        assume x in { F(a) where a be Element of B() : a in { G(b) where b be Element of A() : P[b] } };

        then

        consider a be Element of B() such that

         A1: x = F(a) and

         A2: a in { G(b) where b be Element of A() : P[b] };

        ex b be Element of A() st a = G(b) & P[b] by A2;

        hence thesis by A1;

      end;

      let x be object;

      assume x in { F(G) where a be Element of A() : P[a] };

      then

      consider a be Element of A() such that

       A3: x = F(G) and

       A4: P[a];

      G(a) in { G(b) where b be Element of A() : P[b] } by A4;

      hence thesis by A3;

    end;

    scheme :: QUANTAL1:sch2

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

{ f(a) where a be Element of A() : P[a] } = {}

      provided

       A1: not ex a be Element of A() st P[a];

      assume not thesis;

      then

      reconsider X = { f(a) where a be Element of A() : P[a] } as non empty set;

      set x = the Element of X;

      x in X;

      then ex a be Element of A() st x = f(a) & P[a];

      hence contradiction by A1;

    end;

    deffunc carr( non empty LattStr) = the carrier of $1;

    deffunc join( LattStr) = the L_join of $1;

    deffunc met( LattStr) = the L_meet of $1;

    deffunc times( multMagma) = the multF of $1;

    theorem :: QUANTAL1:1

    for L1,L2 be non empty LattStr st the LattStr of L1 = the LattStr of L2 holds for a1,b1 be Element of L1, a2,b2 be Element of L2 st a1 = a2 & b1 = b2 holds (a1 "\/" b1) = (a2 "\/" b2) & (a1 "/\" b1) = (a2 "/\" b2) & (a1 [= b1 iff a2 [= b2);

    theorem :: QUANTAL1:2



     Th2: for L1,L2 be non empty LattStr st the LattStr of L1 = the LattStr of L2 holds for a be Element of L1, b be Element of L2, X be set st a = b holds (a is_less_than X iff b is_less_than X) & (a is_greater_than X iff b is_greater_than X)

    proof

      let L1,L2 be non empty LattStr such that

       A1: the LattStr of L1 = the LattStr of L2;

      let a be Element of L1, b be Element of L2, X be set such that

       A2: a = b;

      thus a is_less_than X implies b is_less_than X

      proof

        assume

         A3: for c be Element of L1 st c in X holds a [= c;

        let c be Element of L2;

        reconsider d = c as Element of L1 by A1;

        assume c in X;

        then a [= d by A3;

        hence thesis by A1, A2;

      end;

      thus b is_less_than X implies a is_less_than X

      proof

        assume

         A4: for c be Element of L2 st c in X holds b [= c;

        let c be Element of L1;

        reconsider d = c as Element of L2 by A1;

        assume c in X;

        then b [= d by A4;

        hence thesis by A1, A2;

      end;

      thus a is_greater_than X implies b is_greater_than X

      proof

        assume

         A5: for c be Element of L1 st c in X holds c [= a;

        let c be Element of L2;

        reconsider d = c as Element of L1 by A1;

        assume c in X;

        then d [= a by A5;

        hence thesis by A1, A2;

      end;

      assume

       A6: for c be Element of L2 st c in X holds c [= b;

      let c be Element of L1;

      reconsider d = c as Element of L2 by A1;

      assume c in X;

      then d [= b by A6;

      hence thesis by A1, A2;

    end;

    definition

      let L be non empty LattStr, X be Subset of L;

      :: QUANTAL1:def1

      attr X is directed means for Y be finite Subset of X holds ex x be Element of L st ( "\/" (Y,L)) [= x & x in X;

    end

    theorem :: QUANTAL1:3

    for L be non empty LattStr, X be Subset of L st X is directed holds X is non empty

    proof

      let L be non empty LattStr, X be Subset of L;

      assume for Y be finite Subset of X holds ex x be Element of L st ( "\/" (Y,L)) [= x & x in X;

      then ex x be Element of L st ( "\/" (( {} X),L)) [= x & x in X;

      hence thesis;

    end;

    definition

      struct ( LattStr, multMagma) QuantaleStr (# the carrier -> set,

the L_join, L_meet, multF -> BinOp of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty for QuantaleStr;

      existence

      proof

        set A = the non empty set, b1 = the BinOp of A;

        take QuantaleStr (# A, b1, b1, b1 #);

        thus the carrier of QuantaleStr (# A, b1, b1, b1 #) is non empty;

      end;

    end

    definition

      struct ( QuantaleStr, multLoopStr) QuasiNetStr (# the carrier -> set,

the L_join, L_meet, multF -> BinOp of the carrier,

the OneF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty for QuasiNetStr;

      existence

      proof

        set A = the non empty set, b1 = the BinOp of A, e = the Element of A;

        take QuasiNetStr (# A, b1, b1, b1, e #);

        thus the carrier of QuasiNetStr (# A, b1, b1, b1, e #) is non empty;

      end;

    end

    definition

      let IT be non empty multMagma;

      :: QUANTAL1:def2

      attr IT is with_left-zero means ex a be Element of IT st for b be Element of IT holds (a * b) = a;

      :: QUANTAL1:def3

      attr IT is with_right-zero means ex b be Element of IT st for a be Element of IT holds (a * b) = b;

    end

    definition

      let IT be non empty multMagma;

      :: QUANTAL1:def4

      attr IT is with_zero means IT is with_left-zero with_right-zero;

    end

    registration

      cluster with_zero -> with_left-zero with_right-zero for non empty multMagma;

      coherence ;

      cluster with_left-zero with_right-zero -> with_zero for non empty multMagma;

      coherence ;

    end

    registration

      cluster with_zero for non empty multMagma;

      existence

      proof

        set x = the set, f = the BinOp of {x};

        take G = multMagma (# {x}, f #);

        reconsider x as Element of G by TARSKI:def 1;

        thus G is with_left-zero

        proof

          take x;

          thus thesis by TARSKI:def 1;

        end;

        take x;

        thus thesis by TARSKI:def 1;

      end;

    end

    definition

      let IT be non empty QuantaleStr;

      :: QUANTAL1:def5

      attr IT is right-distributive means

      : Def5: for a be Element of IT, X be set holds (a [*] ( "\/" (X,IT))) = ( "\/" ({ (a [*] b) where b be Element of IT : b in X },IT));

      :: QUANTAL1:def6

      attr IT is left-distributive means

      : Def6: for a be Element of IT, X be set holds (( "\/" (X,IT)) [*] a) = ( "\/" ({ (b [*] a) where b be Element of IT : b in X },IT));

      :: QUANTAL1:def7

      attr IT is times-additive means for a,b,c be Element of IT holds ((a "\/" b) [*] c) = ((a [*] c) "\/" (b [*] c)) & (c [*] (a "\/" b)) = ((c [*] a) "\/" (c [*] b));

      :: QUANTAL1:def8

      attr IT is times-continuous means for X1,X2 be Subset of IT st X1 is directed & X2 is directed holds (( "\/" X1) [*] ( "\/" X2)) = ( "\/" ({ (a [*] b) where a be Element of IT, b be Element of IT : a in X1 & b in X2 },IT));

    end

    reserve x,y,z for set;

    theorem :: QUANTAL1:4



     Th4: for Q be non empty QuantaleStr st the LattStr of Q = ( BooleLatt {} ) holds Q is associative commutative unital with_zero complete right-distributive left-distributive Lattice-like

    proof

      set B = ( BooleLatt {} );

      let Q be non empty QuantaleStr;

      set a = the Element of Q;

      assume

       A1: the LattStr of Q = B;

       A2:

      now

        let x,y be Element of Q;



         A3: carr(B) = { {} } by LATTICE3:def 1, ZFMISC_1: 1;

        then x = {} by A1, TARSKI:def 1;

        hence x = y by A1, A3, TARSKI:def 1;

      end;

      set o = times(Q);

      thus times(Q) is associative

      proof

        thus for a,b,c be Element of Q holds (o . (a,(o . (b,c)))) = (o . ((o . (a,b)),c)) by A2;

      end;



       A4: (for p,q,r be Element of Q holds (p "/\" (q "/\" r)) = ((p "/\" q) "/\" r)) & for p,q be Element of Q holds (p "/\" (p "\/" q)) = p by A2;

      thus times(Q) is commutative

      proof

        thus for a,b be Element of Q holds (o . (a,b)) = (o . (b,a)) by A2;

      end;

      thus times(Q) is having_a_unity

      proof

        take a;

        thus a is_a_left_unity_wrt times(Q)

        proof

          let b be Element of Q;

          thus ( times(Q) . (a,b)) = b by A2;

        end;

        let b be Element of Q;

        thus ( times(Q) . (b,a)) = b by A2;

      end;

      thus Q is with_zero

      proof

        thus Q is with_left-zero

        proof

          take a;

          thus thesis by A2;

        end;

        take a;

        thus thesis by A2;

      end;

      now

        let X be set;

        consider p be Element of B such that

         A5: X is_less_than p and

         A6: for r be Element of B st X is_less_than r holds p [= r by LATTICE3:def 18;

        reconsider p9 = p as Element of Q by A1;

        take p9;

        thus X is_less_than p9 by A1, A5, Th2;

        let r9 be Element of Q;

        reconsider r = r9 as Element of B by A1;

        assume X is_less_than r9;

        then X is_less_than r by A1, Th2;

        then p [= r by A6;

        hence p9 [= r9 by A1;

      end;

      hence for X be set holds ex p be Element of Q st X is_less_than p & for r be Element of Q st X is_less_than r holds p [= r;

      thus Q is right-distributive by A2;

      thus Q is left-distributive by A2;



       A7: (for p,q be Element of Q holds ((p "/\" q) "\/" q) = q) & for p,q be Element of Q holds (p "/\" q) = (q "/\" p) by A2;

      (for p,q be Element of Q holds (p "\/" q) = (q "\/" p)) & for p,q,r be Element of Q holds (p "\/" (q "\/" r)) = ((p "\/" q) "\/" r) by A2;

      then Q is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A7, A4;

      hence thesis;

    end;

    registration

      let A be non empty set, b1,b2,b3 be BinOp of A;

      cluster QuantaleStr (# A, b1, b2, b3 #) -> non empty;

      coherence ;

    end

    registration

      cluster associative commutative unital with_zero left-distributive right-distributive complete Lattice-like for non empty QuantaleStr;

      existence

      proof

        set B = ( BooleLatt {} );

        set b = the BinOp of B;

        take QuantaleStr (# carr(B), join(B), met(B), b #);

        thus thesis by Th4;

      end;

    end

    scheme :: QUANTAL1:sch3

    LUBFraenkelDistr { Q() -> complete Lattice-like non empty QuantaleStr , f( set, set) -> Element of Q() , X,Y() -> set } :

( "\/" ({ ( "\/" ({ f(a,b) where b be Element of Q() : b in Y() },Q())) where a be Element of Q() : a in X() },Q())) = ( "\/" ({ f(a,b) where a be Element of Q(), b be Element of Q() : a in X() & b in Y() },Q()));

      set Q = Q(), X = X(), Y = Y();

      set Z = { { f(a,b) where b be Element of Q : b in Y } where a be Element of Q : a in X };

      set W = { ( "\/" V) where V be Subset of Q : V in Z };

      set S = { f(a,b) where a be Element of Q, b be Element of Q : a in X & b in Y };



       A1: W = { ( "\/" ({ f(a,b) where b be Element of Q : b in Y },Q)) where a be Element of Q : a in X }

      proof

        thus W c= { ( "\/" ({ f(a,b) where b be Element of Q : b in Y },Q)) where a be Element of Q : a in X }

        proof

          let x be object;

          assume x in W;

          then

          consider V be Subset of Q such that

           A2: x = ( "\/" V) and

           A3: V in Z;

          ex a be Element of Q st V = { f(a,b) where b be Element of Q : b in Y } & a in X by A3;

          hence thesis by A2;

        end;

        let x be object;

        assume x in { ( "\/" ({ f(a,b) where b be Element of Q : b in Y },Q)) where a be Element of Q : a in X };

        then

        consider a be Element of Q such that

         A4: x = ( "\/" ({ f(a,b) where b be Element of Q : b in Y },Q)) and

         A5: a in X;



         A6: { f(a,b) where b be Element of Q : b in Y } c= carr(Q)

        proof

          let y be object;

          assume y in { f(a,b) where b be Element of Q : b in Y };

          then ex b be Element of Q st y = f(a,b) & b in Y;

          hence thesis;

        end;

        { f(a,c) where c be Element of Q : c in Y } in Z by A5;

        hence thesis by A4, A6;

      end;



       A7: S = ( union Z)

      proof

        thus S c= ( union Z)

        proof

          let x be object;

          assume x in S;

          then

          consider a,b be Element of Q such that

           A8: x = f(a,b) & a in X & b in Y;

          x in { f(a,c) where c be Element of Q : c in Y } & { f(a,d) where d be Element of Q : d in Y } in Z by A8;

          hence thesis by TARSKI:def 4;

        end;

        let x be object;

        assume x in ( union Z);

        then

        consider V be set such that

         A9: x in V and

         A10: V in Z by TARSKI:def 4;

        consider a be Element of Q such that

         A11: V = { f(a,b) where b be Element of Q : b in Y } and

         A12: a in X by A10;

        ex b be Element of Q st x = f(a,b) & b in Y by A9, A11;

        hence thesis by A12;

      end;

      Z c= ( bool carr(Q))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in Z;

        then

        consider a be Element of Q such that

         A13: x = { f(a,b) where b be Element of Q : b in Y } and a in X;

        xx c= carr(Q)

        proof

          let y be object;

          assume y in xx;

          then ex b be Element of Q st y = f(a,b) & b in Y by A13;

          hence thesis;

        end;

        hence thesis;

      end;

      hence thesis by A1, A7, LATTICE3: 48;

    end;

    reserve Q for left-distributive right-distributive complete Lattice-like non empty QuantaleStr,

a,b,c,d for Element of Q;

    theorem :: QUANTAL1:5



     Th5: for Q holds for X,Y be set holds (( "\/" (X,Q)) [*] ( "\/" (Y,Q))) = ( "\/" ({ (a [*] b) : a in X & b in Y },Q))

    proof

      let Q;

      let X,Y be set;

      deffunc F( Element of Q) = ($1 [*] ( "\/" (Y,Q)));

      deffunc G( Element of Q) = ( "\/" ({ ($1 [*] b) : b in Y },Q));

      defpred P[ set] means $1 in X;

      deffunc H( Element of Q, Element of Q) = ($1 [*] $2);



       A1: for a holds F(a) = G(a) by Def5;

      { F(c) : P[c] } = { G(a) : P[a] } from FRAENKEL:sch 5( A1);



      hence (( "\/" (X,Q)) [*] ( "\/" (Y,Q))) = ( "\/" ({ ( "\/" ({ H(a,b) where b be Element of Q : b in Y },Q)) where a be Element of Q : a in X },Q)) by Def6

      .= ( "\/" ({ H(c,d) where c be Element of Q, d be Element of Q : c in X & d in Y },Q)) from LUBFraenkelDistr;

    end;

    theorem :: QUANTAL1:6



     Th6: ((a "\/" b) [*] c) = ((a [*] c) "\/" (b [*] c)) & (c [*] (a "\/" b)) = ((c [*] a) "\/" (c [*] b))

    proof

      set X1 = { (d [*] c) : d in {a, b} }, X2 = { (c [*] d) : d in {a, b} };

      now

        let x be object;

        a in {a, b} & b in {a, b} by TARSKI:def 2;

        hence x = (a [*] c) or x = (b [*] c) implies x in X1;

        assume x in X1;

        then ex d st x = (d [*] c) & d in {a, b};

        hence x = (a [*] c) or x = (b [*] c) by TARSKI:def 2;

      end;

      then

       A1: X1 = {(a [*] c), (b [*] c)} by TARSKI:def 2;

      now

        let x be object;

        a in {a, b} & b in {a, b} by TARSKI:def 2;

        hence x = (c [*] a) or x = (c [*] b) implies x in X2;

        assume x in X2;

        then ex d st x = (c [*] d) & d in {a, b};

        hence x = (c [*] a) or x = (c [*] b) by TARSKI:def 2;

      end;

      then

       A2: X2 = {(c [*] a), (c [*] b)} by TARSKI:def 2;



       A3: (a "\/" b) = ( "\/" {a, b}) by LATTICE3: 43;

      then ((a "\/" b) [*] c) = ( "\/" (X1,Q)) by Def6;

      hence ((a "\/" b) [*] c) = ((a [*] c) "\/" (b [*] c)) by A1, LATTICE3: 43;

      (c [*] (a "\/" b)) = ( "\/" (X2,Q)) by A3, Def5;

      hence thesis by A2, LATTICE3: 43;

    end;

    registration

      let A be non empty set, b1,b2,b3 be BinOp of A, e be Element of A;

      cluster QuasiNetStr (# A, b1, b2, b3, e #) -> non empty;

      coherence ;

    end

    registration

      cluster complete Lattice-like for non empty QuasiNetStr;

      existence

      proof

        set B = ( BooleLatt {} );

        set e = the Element of B, b = the BinOp of B;

        take QuasiNetStr (# carr(B), join(B), met(B), b, e #);

        thus thesis by Th4;

      end;

    end

    registration

      cluster left-distributive right-distributive -> times-continuous times-additive for complete Lattice-like non empty QuasiNetStr;

      coherence by Th5, Th6;

    end

    registration

      cluster associative commutative unital with_zero with_left-zero left-distributive right-distributive complete Lattice-like for non empty QuasiNetStr;

      existence

      proof

        set B = ( BooleLatt {} );

        set e = the Element of B, b = the BinOp of B;

        take Q = QuasiNetStr (# carr(B), join(B), met(B), b, e #);

        Q is with_zero unital by Th4;

        hence thesis by Th4;

      end;

    end

    definition

      mode Quantale is associative left-distributive right-distributive complete Lattice-like non empty QuantaleStr;

      mode QuasiNet is unital associative with_left-zero times-continuous times-additive complete Lattice-like non empty QuasiNetStr;

    end

    definition

      mode BlikleNet is with_zero non empty QuasiNet;

    end

    theorem :: QUANTAL1:7

    for Q be unital non empty QuasiNetStr st Q is Quantale holds Q is BlikleNet

    proof

      defpred P[ set] means $1 in {} ;

      let Q be unital non empty QuasiNetStr;

      assume Q is Quantale;

      then

      reconsider Q9 = Q as Quantale;



       A1: ( Bottom Q9) = ( "\/" ( {} ,Q9)) by LATTICE3: 49;



       A2: not ex c be Element of Q9 st P[c];

      Q9 is with_zero

      proof

        hereby

          reconsider a = ( Bottom Q9) as Element of Q9;

          take a;

          let b be Element of Q9;

          deffunc F1( Element of Q9) = ($1 [*] b);

          { F1(c) where c be Element of Q9 : P[c] } = {} from EmptyFraenkel( A2);

          hence (a [*] b) = a by A1, Def6;

        end;

        take ( Bottom Q9);

        let a be Element of Q9;

        deffunc F2( Element of Q9) = (a [*] $1);

        { F2(c) where c be Element of Q9 : P[c] } = {} from EmptyFraenkel( A2);

        hence thesis by A1, Def5;

      end;

      hence thesis;

    end;

    reserve Q for Quantale,

a,a9,b,b9,c,d,d1,d2,D for Element of Q;

    theorem :: QUANTAL1:8



     Th8: a [= b implies (a [*] c) [= (b [*] c) & (c [*] a) [= (c [*] b) by Th6;

    theorem :: QUANTAL1:9



     Th9: a [= b & c [= d implies (a [*] c) [= (b [*] d)

    proof

      assume a [= b & c [= d;

      then (a [*] c) [= (b [*] c) & (b [*] c) [= (b [*] d) by Th8;

      hence thesis by LATTICES: 7;

    end;

    definition

      let f be Function;

      :: QUANTAL1:def9

      attr f is idempotent means (f * f) = f;

    end



     Lm1: for A be non empty set, f be UnOp of A st f is idempotent holds for a be Element of A holds (f . (f . a)) = (f . a) by FUNCT_2: 15;

    definition

      let L be non empty LattStr;

      let IT be UnOp of L;

      :: QUANTAL1:def10

      attr IT is inflationary means for p be Element of L holds p [= (IT . p);

      :: QUANTAL1:def11

      attr IT is deflationary means for p be Element of L holds (IT . p) [= p;

      :: QUANTAL1:def12

      attr IT is monotone means for p,q be Element of L st p [= q holds (IT . p) [= (IT . q);

      :: QUANTAL1:def13

      attr IT is \/-distributive means for X be Subset of L holds (IT . ( "\/" X)) [= ( "\/" ({ (IT . a) where a be Element of L : a in X },L));

    end

    registration

      let L be Lattice;

      cluster inflationary deflationary monotone for UnOp of L;

      existence

      proof

        reconsider f = ( id the carrier of L) as UnOp of L;

        take f;

        thus f is inflationary

        proof

          let p be Element of L;

          thus thesis;

        end;

        thus f is deflationary

        proof

          let p be Element of L;

          thus thesis;

        end;

        let p,q be Element of L;

        thus thesis;

      end;

    end

    theorem :: QUANTAL1:10



     Th10: for L be complete Lattice, j be UnOp of L st j is monotone holds j is \/-distributive iff for X be Subset of L holds (j . ( "\/" X)) = ( "\/" ({ (j . a) where a be Element of L : a in X },L))

    proof

      let L be complete Lattice, j be UnOp of L such that

       A1: j is monotone;

      thus j is \/-distributive implies for X be Subset of L holds (j . ( "\/" X)) = ( "\/" ({ (j . a) where a be Element of L : a in X },L))

      proof

        assume

         A2: for X be Subset of L holds (j . ( "\/" X)) [= ( "\/" ({ (j . a) where a be Element of L : a in X },L));

        let X be Subset of L;

        { (j . a) where a be Element of L : a in X } is_less_than (j . ( "\/" X))

        proof

          let x be Element of L;

          assume x in { (j . a) where a be Element of L : a in X };

          then

          consider a be Element of L such that

           A3: x = (j . a) and

           A4: a in X;

          a [= ( "\/" X) by A4, LATTICE3: 38;

          hence thesis by A1, A3;

        end;

        then

         A5: ( "\/" ({ (j . a) where a be Element of L : a in X },L)) [= (j . ( "\/" X)) by LATTICE3:def 21;

        (j . ( "\/" X)) [= ( "\/" ({ (j . a) where a be Element of L : a in X },L)) by A2;

        hence thesis by A5, LATTICES: 8;

      end;

      assume

       A6: for X be Subset of L holds (j . ( "\/" X)) = ( "\/" ({ (j . a) where a be Element of L : a in X },L));

      let X be Subset of L;

      (j . ( "\/" X)) [= (j . ( "\/" X));

      hence thesis by A6;

    end;

    definition

      let Q be non empty QuantaleStr;

      let IT be UnOp of Q;

      :: QUANTAL1:def14

      attr IT is times-monotone means for a,b be Element of Q holds ((IT . a) [*] (IT . b)) [= (IT . (a [*] b));

    end

    definition

      let Q be non empty QuantaleStr, a,b be Element of Q;

      :: QUANTAL1:def15

      func a -r> b -> Element of Q equals ( "\/" ({ c where c be Element of Q : (c [*] a) [= b },Q));

      correctness ;

      :: QUANTAL1:def16

      func a -l> b -> Element of Q equals ( "\/" ({ c where c be Element of Q : (a [*] c) [= b },Q));

      correctness ;

    end

    theorem :: QUANTAL1:11



     Th11: (a [*] b) [= c iff b [= (a -l> c)

    proof

      set X = { d : (a [*] d) [= c };

      X c= carr(Q)

      proof

        let x be object;

        assume x in X;

        then ex d st x = d & (a [*] d) [= c;

        hence thesis;

      end;

      then

      reconsider X as Subset of Q;

      thus (a [*] b) [= c implies b [= (a -l> c)

      proof

        assume (a [*] b) [= c;

        then b in X;

        hence thesis by LATTICE3: 38;

      end;

      deffunc F( Element of Q) = (a [*] $1);

      defpred P1[ set] means $1 in X;

      defpred P2[ Element of Q] means (a [*] $1) [= c;

      assume b [= (a -l> c);

      then

       A1: (a [*] b) [= (a [*] ( "\/" X)) by Th8;

      now

        let d;

        assume d in X;

        then ex d1 st d = d1 & (a [*] d1) [= c;

        hence (a [*] d) [= c;

      end;

      then

       A2: P1[d] iff P2[d];



       A3: { F(d1) : P1[d1] } = { F(d2) : P2[d2] } from FRAENKEL:sch 3( A2);



       A4: { (a [*] d) : d in X } is_less_than c

      proof

        let d1;

        assume d1 in { (a [*] d) : d in X };

        then ex d2 st d1 = (a [*] d2) & (a [*] d2) [= c by A3;

        hence thesis;

      end;

      (a [*] ( "\/" X)) = ( "\/" ({ (a [*] d) : d in X },Q)) by Def5;

      then (a [*] ( "\/" X)) [= c by A4, LATTICE3:def 21;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: QUANTAL1:12



     Th12: (a [*] b) [= c iff a [= (b -r> c)

    proof

      set X = { d : (d [*] b) [= c };

      X c= carr(Q)

      proof

        let x be object;

        assume x in X;

        then ex d st x = d & (d [*] b) [= c;

        hence thesis;

      end;

      then

      reconsider X as Subset of Q;

      thus (a [*] b) [= c implies a [= (b -r> c)

      proof

        assume (a [*] b) [= c;

        then a in X;

        hence thesis by LATTICE3: 38;

      end;

      deffunc F( Element of Q) = ($1 [*] b);

      defpred P1[ set] means $1 in X;

      defpred P2[ Element of Q] means ($1 [*] b) [= c;

      assume a [= (b -r> c);

      then

       A1: (a [*] b) [= (( "\/" X) [*] b) by Th8;

      now

        let d;

        assume d in X;

        then ex d1 st d = d1 & (d1 [*] b) [= c;

        hence (d [*] b) [= c;

      end;

      then

       A2: P1[d] iff P2[d];



       A3: { F(d1) : P1[d1] } = { F(d2) : P2[d2] } from FRAENKEL:sch 3( A2);



       A4: { (d [*] b) : d in X } is_less_than c

      proof

        let d1;

        assume d1 in { (d [*] b) : d in X };

        then ex d2 st d1 = (d2 [*] b) & (d2 [*] b) [= c by A3;

        hence thesis;

      end;

      (( "\/" X) [*] b) = ( "\/" ({ (d [*] b) : d in X },Q)) by Def6;

      then (( "\/" X) [*] b) [= c by A4, LATTICE3:def 21;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: QUANTAL1:13



     Th13: for Q be Quantale, s,a,b be Element of Q st a [= b holds (b -r> s) [= (a -r> s) & (b -l> s) [= (a -l> s)

    proof

      let Q be Quantale, s,a,b be Element of Q such that

       A1: a [= b;

      { d where d be Element of Q : (d [*] b) [= s } c= { c where c be Element of Q : (c [*] a) [= s }

      proof

        let x be object;

        assume x in { d where d be Element of Q : (d [*] b) [= s };

        then

        consider d be Element of Q such that

         A2: x = d and

         A3: (d [*] b) [= s;

        (d [*] a) [= (d [*] b) by A1, Th8;

        then (d [*] a) [= s by A3, LATTICES: 7;

        hence thesis by A2;

      end;

      hence (b -r> s) [= (a -r> s) by LATTICE3: 45;

      { d where d be Element of Q : (b [*] d) [= s } c= { c where c be Element of Q : (a [*] c) [= s }

      proof

        let x be object;

        assume x in { d where d be Element of Q : (b [*] d) [= s };

        then

        consider d be Element of Q such that

         A4: x = d and

         A5: (b [*] d) [= s;

        (a [*] d) [= (b [*] d) by A1, Th8;

        then (a [*] d) [= s by A5, LATTICES: 7;

        hence thesis by A4;

      end;

      hence thesis by LATTICE3: 45;

    end;

    theorem :: QUANTAL1:14

    for Q be Quantale, s be Element of Q, j be UnOp of Q st for a be Element of Q holds (j . a) = ((a -r> s) -r> s) holds j is monotone

    proof

      let Q be Quantale, s be Element of Q;

      let j be UnOp of Q such that

       A1: for a be Element of Q holds (j . a) = ((a -r> s) -r> s);

      thus j is monotone

      proof

        let a,b be Element of Q;

        assume a [= b;

        then (b -r> s) [= (a -r> s) by Th13;

        then

         A2: ((a -r> s) -r> s) [= ((b -r> s) -r> s) by Th13;

        ((a -r> s) -r> s) = (j . a) by A1;

        hence thesis by A1, A2;

      end;

    end;

    definition

      let Q be non empty QuantaleStr;

      let IT be Element of Q;

      :: QUANTAL1:def17

      attr IT is dualizing means for a be Element of Q holds ((a -r> IT) -l> IT) = a & ((a -l> IT) -r> IT) = a;

      :: QUANTAL1:def18

      attr IT is cyclic means for a be Element of Q holds (a -r> IT) = (a -l> IT);

    end

    theorem :: QUANTAL1:15



     Th15: c is cyclic iff for a, b st (a [*] b) [= c holds (b [*] a) [= c

    proof

      thus c is cyclic implies for a, b st (a [*] b) [= c holds (b [*] a) [= c

      proof

        assume

         A1: (a -r> c) = (a -l> c);

        let a, b;

        assume (a [*] b) [= c;

        then a [= (b -r> c) by Th12;

        then a [= (b -l> c) by A1;

        hence thesis by Th11;

      end;

      assume

       A2: (a [*] b) [= c implies (b [*] a) [= c;

      let a;

      set X1 = { d1 : (d1 [*] a) [= c }, X2 = { d2 : (a [*] d2) [= c };

      X1 = X2

      proof

        thus X1 c= X2

        proof

          let x be object;

          assume x in X1;

          then

          consider d such that

           A3: x = d and

           A4: (d [*] a) [= c;

          (a [*] d) [= c by A2, A4;

          hence thesis by A3;

        end;

        let x be object;

        assume x in X2;

        then

        consider d such that

         A5: x = d and

         A6: (a [*] d) [= c;

        (d [*] a) [= c by A2, A6;

        hence thesis by A5;

      end;

      hence thesis;

    end;

    theorem :: QUANTAL1:16



     Th16: for Q be Quantale, s,a be Element of Q st s is cyclic holds a [= ((a -r> s) -r> s) & a [= ((a -l> s) -l> s)

    proof

      let Q;

      let s,a be Element of Q such that

       A1: s is cyclic;



       A2: { b : b [= a } c= { c : (c [*] (a -r> s)) [= s }

      proof

        let x be object;

        assume x in { b : b [= a };

        then

        consider b such that

         A3: x = b and

         A4: b [= a;

        ((b -r> s) [*] b) [= s by Th12;

        then

         A5: (b [*] (b -r> s)) [= s by A1, Th15;

        (a -r> s) [= (b -r> s) by A4, Th13;

        then (b [*] (a -r> s)) [= (b [*] (b -r> s)) by Th8;

        then (b [*] (a -r> s)) [= s by A5, LATTICES: 7;

        hence thesis by A3;

      end;



       A6: { b : b [= a } c= { c : ((a -l> s) [*] c) [= s }

      proof

        let x be object;

        assume x in { b : b [= a };

        then

        consider b such that

         A7: x = b and

         A8: b [= a;

        (b [*] (b -l> s)) [= s by Th11;

        then

         A9: ((b -l> s) [*] b) [= s by A1, Th15;

        (a -l> s) [= (b -l> s) by A8, Th13;

        then ((a -l> s) [*] b) [= ((b -l> s) [*] b) by Th8;

        then ((a -l> s) [*] b) [= s by A9, LATTICES: 7;

        hence thesis by A7;

      end;

      a = ( "\/" ({ d : d [= a },Q)) by LATTICE3: 44;

      hence a [= ((a -r> s) -r> s) by A2, LATTICE3: 45;

      a = ( "\/" ({ d : d [= a },Q)) by LATTICE3: 44;

      hence thesis by A6, LATTICE3: 45;

    end;

    theorem :: QUANTAL1:17

    for Q be Quantale, s,a be Element of Q st s is cyclic holds (a -r> s) = (((a -r> s) -r> s) -r> s) & (a -l> s) = (((a -l> s) -l> s) -l> s)

    proof

      let Q;

      let s,a be Element of Q;

      assume

       A1: s is cyclic;

      then a [= ((a -r> s) -r> s) by Th16;

      then

       A2: (((a -r> s) -r> s) -r> s) [= (a -r> s) by Th13;

      a [= ((a -l> s) -l> s) by A1, Th16;

      then

       A3: (((a -l> s) -l> s) -l> s) [= (a -l> s) by Th13;

      (a -r> s) [= (((a -r> s) -r> s) -r> s) & (a -l> s) [= (((a -l> s) -l> s) -l> s) by A1, Th16;

      hence thesis by A2, A3, LATTICES: 8;

    end;

    theorem :: QUANTAL1:18

    for Q be Quantale, s,a,b be Element of Q holds (((a -r> s) -r> s) [*] ((b -r> s) -r> s)) [= (((a [*] b) -r> s) -r> s)

    proof

      let Q;

      let s,a,b be Element of Q;

      deffunc NEG( Element of Q) = { c : (c [*] ($1 -r> s)) [= s };



       A1: { (a9 [*] b9) : a9 in NEG(a) & b9 in NEG(b) } c= NEG([*])

      proof

        defpred P[ Element of Q] means ($1 [*] (a [*] b)) [= s;

        deffunc G( Element of Q) = $1;

        let x be object;

        set A = { G(c) : P[c] };

        assume x in { (a9 [*] b9) : a9 in NEG(a) & b9 in NEG(b) };

        then

        consider a9, b9 such that

         A2: x = (a9 [*] b9) and

         A3: a9 in NEG(a) and

         A4: b9 in NEG(b);

        deffunc F( Element of Q) = ((a9 [*] b9) [*] $1);

        set B = { F(G) : P[c] };



         A5: ex c st b9 = c & (c [*] (b -r> s)) [= s by A4;



         A6: ex c st a9 = c & (c [*] (a -r> s)) [= s by A3;



         A7: B is_less_than s

        proof

          let d;

          assume d in B;

          then

          consider c such that

           A8: d = ((a9 [*] b9) [*] c) and

           A9: (c [*] (a [*] b)) [= s;



           A10: (b -r> s) [= (b9 -l> s) by A5, Th11;

          ((c [*] a) [*] b) [= s by A9, GROUP_1:def 3;

          then (c [*] a) [= (b -r> s) by Th12;

          then (c [*] a) [= (b9 -l> s) by A10, LATTICES: 7;

          then (b9 [*] (c [*] a)) [= s by Th11;

          then ((b9 [*] c) [*] a) [= s by GROUP_1:def 3;

          then

           A11: (b9 [*] c) [= (a -r> s) by Th12;

          (a -r> s) [= (a9 -l> s) by A6, Th11;

          then (b9 [*] c) [= (a9 -l> s) by A11, LATTICES: 7;

          then (a9 [*] (b9 [*] c)) [= s by Th11;

          hence d [= s by A8, GROUP_1:def 3;

        end;

        { F(c) : c in A } = B from DenestFraenkel;

        then ((a9 [*] b9) [*] ((a [*] b) -r> s)) = ( "\/" (B,Q)) by Def5;

        then ((a9 [*] b9) [*] ((a [*] b) -r> s)) [= s by A7, LATTICE3:def 21;

        hence thesis by A2;

      end;

      (((a -r> s) -r> s) [*] ((b -r> s) -r> s)) = ( "\/" ({ (a9 [*] b9) : a9 in NEG(a) & b9 in NEG(b) },Q)) by Th5;

      hence thesis by A1, LATTICE3: 45;

    end;

    theorem :: QUANTAL1:19



     Th19: D is dualizing implies Q is unital & ( the_unity_wrt the multF of Q) = (D -r> D) & ( the_unity_wrt the multF of Q) = (D -l> D)

    proof

      set I = (D -l> D), J = (D -r> D);

      assume

       A1: ((a -r> D) -l> D) = a & ((a -l> D) -r> D) = a;

       A2:

      now

        deffunc F( set) = $1;

        let a;

        defpred P1[ Element of Q] means ($1 [*] (a [*] I)) [= D;

        defpred P2[ Element of Q] means ($1 [*] a) [= D;

        defpred P3[ Element of Q] means ((J [*] a) [*] $1) [= D;

        defpred P4[ Element of Q] means (a [*] $1) [= D;



         A3: P1[b] iff P2[b]

        proof

          (b [*] (a [*] I)) = ((b [*] a) [*] I) & (I -r> D) = D by A1, GROUP_1:def 3;

          hence thesis by Th12;

        end;



         A4: { F(b) : P1[b] } = { F(c) : P2[c] } from FRAENKEL:sch 3( A3);



        thus (a [*] I) = (((a [*] I) -r> D) -l> D) by A1

        .= ((a -r> D) -l> D) by A4

        .= a by A1;



         A5: P3[b] iff P4[b]

        proof

          (J [*] (a [*] b)) = ((J [*] a) [*] b) & (J -l> D) = D by A1, GROUP_1:def 3;

          hence thesis by Th11;

        end;



         A6: { F(b) : P3[b] } = { F(c) : P4[c] } from FRAENKEL:sch 3( A5);



        thus (J [*] a) = (((J [*] a) -l> D) -r> D) by A1

        .= ((a -l> D) -r> D) by A6

        .= a by A1;

      end;



       A7: I is_a_right_unity_wrt times(Q)

      proof

        let a;



        thus ( times(Q) . (a,I)) = (a [*] I)

        .= a by A2;

      end;



       A8: I = (J [*] I) by A2;

      I is_a_left_unity_wrt times(Q)

      proof

        let a;



        thus ( times(Q) . (I,a)) = (J [*] a) by A2, A8

        .= a by A2;

      end;

      then

       A9: I is_a_unity_wrt times(Q) by A7;

      hence times(Q) is having_a_unity;

      J = (J [*] I) by A2;

      hence thesis by A8, A9, BINOP_1:def 8;

    end;

    theorem :: QUANTAL1:20

    a is dualizing implies (b -r> c) = ((b [*] (c -l> a)) -r> a) & (b -l> c) = (((c -r> a) [*] b) -l> a)

    proof

      deffunc F( set) = $1;

      defpred P1[ Element of Q] means ($1 [*] b) [= c;

      defpred P2[ Element of Q] means ($1 [*] (b [*] (c -l> a))) [= a;

      defpred P3[ Element of Q] means (b [*] $1) [= c;

      defpred P4[ Element of Q] means (((c -r> a) [*] b) [*] $1) [= a;

      assume

       A1: ((d -r> a) -l> a) = d & ((d -l> a) -r> a) = d;

      then

       A2: c = ((c -l> a) -r> a);



       A3: P1[d] iff P2[d]

      proof

        (d [*] (b [*] (c -l> a))) = ((d [*] b) [*] (c -l> a)) by GROUP_1:def 3;

        hence thesis by A2, Th12;

      end;

      { F(d1) : P1[d1] } = { F(d2) : P2[d2] } from FRAENKEL:sch 3( A3);

      hence (b -r> c) = ((b [*] (c -l> a)) -r> a);



       A4: c = ((c -r> a) -l> a) by A1;



       A5: P3[d] iff P4[d]

      proof

        (((c -r> a) [*] b) [*] d) = ((c -r> a) [*] (b [*] d)) by GROUP_1:def 3;

        hence thesis by A4, Th11;

      end;

      { F(d1) : P3[d1] } = { F(d2) : P4[d2] } from FRAENKEL:sch 3( A5);

      hence thesis;

    end;

    definition

      struct ( QuasiNetStr) Girard-QuantaleStr (# the carrier -> set,

the L_join, L_meet, multF -> BinOp of the carrier,

the OneF, absurd -> Element of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty for Girard-QuantaleStr;

      existence

      proof

        set A = the non empty set, b1 = the BinOp of A, e1 = the Element of A;

        take Girard-QuantaleStr (# A, b1, b1, b1, e1, e1 #);

        thus the carrier of Girard-QuantaleStr (# A, b1, b1, b1, e1, e1 #) is non empty;

      end;

    end

    definition

      let IT be non empty Girard-QuantaleStr;

      :: QUANTAL1:def19

      attr IT is cyclic means

      : Def19: the absurd of IT is cyclic;

      :: QUANTAL1:def20

      attr IT is dualized means

      : Def20: the absurd of IT is dualizing;

    end

    theorem :: QUANTAL1:21



     Th21: for Q be non empty Girard-QuantaleStr st the LattStr of Q = ( BooleLatt {} ) holds Q is cyclic dualized

    proof

      let Q be non empty Girard-QuantaleStr;

      set c = the absurd of Q;

      assume the LattStr of Q = ( BooleLatt {} );

      then

       A1: carr(Q) = { {} } by LATTICE3:def 1, ZFMISC_1: 1;

      thus Q is cyclic

      proof

        let a be Element of Q;

        (a -r> c) = {} by A1, TARSKI:def 1;

        hence thesis by A1, TARSKI:def 1;

      end;

      let a be Element of Q;

      ((a -r> c) -l> c) = {} & ((a -l> c) -r> c) = {} by A1, TARSKI:def 1;

      hence thesis by A1, TARSKI:def 1;

    end;

    registration

      let A be non empty set, b1,b2,b3 be BinOp of A, e1,e2 be Element of A;

      cluster Girard-QuantaleStr (# A, b1, b2, b3, e1, e2 #) -> non empty;

      coherence ;

    end

    registration

      cluster associative commutative unital left-distributive right-distributive complete Lattice-like cyclic dualized strict for non empty Girard-QuantaleStr;

      existence

      proof

        set B = ( BooleLatt {} );

        set b = the BinOp of B;

        set e = the Element of B;

        take Girard-QuantaleStr (# carr(B), join(B), met(B), b, e, e #);

        thus thesis by Th4, Th21;

      end;

    end

    definition

      mode Girard-Quantale is associative unital left-distributive right-distributive complete Lattice-like cyclic dualized non empty Girard-QuantaleStr;

    end

    definition

      let G be Girard-QuantaleStr;

      :: QUANTAL1:def21

      func Bottom G -> Element of G equals the absurd of G;

      correctness ;

    end

    definition

      let G be non empty Girard-QuantaleStr;

      :: QUANTAL1:def22

      func Top G -> Element of G equals (( Bottom G) -r> ( Bottom G));

      correctness ;

      let a be Element of G;

      :: QUANTAL1:def23

      func Bottom a -> Element of G equals (a -r> ( Bottom G));

      correctness ;

    end

    definition

      let G be non empty Girard-QuantaleStr;

      :: QUANTAL1:def24

      func Negation G -> UnOp of G means for a be Element of G holds (it . a) = ( Bottom a);

      existence

      proof

        deffunc F( Element of G) = ( Bottom $1);

        consider f be Function of the carrier of G, the carrier of G such that

         A1: for a be Element of G holds (f . a) = F(a) from FUNCT_2:sch 4;

        reconsider f as UnOp of G;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be UnOp of G such that

         A2: for a be Element of G holds (f1 . a) = ( Bottom a) and

         A3: for a be Element of G holds (f2 . a) = ( Bottom a);

        now

          let a be Element of G;



          thus (f1 . a) = ( Bottom a) by A2

          .= (f2 . a) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let G be non empty Girard-QuantaleStr, u be UnOp of G;

      :: QUANTAL1:def25

      func Bottom u -> UnOp of G equals (( Negation G) * u);

      correctness ;

    end

    definition

      let G be non empty Girard-QuantaleStr, o be BinOp of G;

      :: QUANTAL1:def26

      func Bottom o -> BinOp of G equals (( Negation G) * o);

      correctness ;

    end

    reserve Q for Girard-Quantale,

a,a1,a2,b,b1,b2,c,d for Element of Q,

X for set;

    theorem :: QUANTAL1:22



     Th22: ( Bottom ( Bottom a)) = a

    proof

      the absurd of Q is cyclic by Def19;

      then

       A1: (a -l> the absurd of Q) = (a -r> the absurd of Q);

      the absurd of Q is dualizing by Def20;

      hence thesis by A1;

    end;

    theorem :: QUANTAL1:23

    a [= b implies ( Bottom b) [= ( Bottom a) by Th13;

    theorem :: QUANTAL1:24



     Th24: ( Bottom ( "\/" (X,Q))) = ( "/\" ({ ( Bottom a) : a in X },Q))

    proof

      { (( "/\" ({ ( Bottom a) : a in X },Q)) [*] b) : b in X } is_less_than ( Bottom Q)

      proof

        let c;

        assume c in { (( "/\" ({ ( Bottom a) : a in X },Q)) [*] b) : b in X };

        then

        consider b such that

         A1: c = (( "/\" ({ ( Bottom a) : a in X },Q)) [*] b) & b in X;

        ( Bottom b) in { ( Bottom a) : a in X } by A1;

        then ( "/\" ({ ( Bottom a) : a in X },Q)) [= ( Bottom b) by LATTICE3: 38;

        hence c [= ( Bottom Q) by A1, Th12;

      end;

      then ( "\/" ({ (( "/\" ({ ( Bottom a) : a in X },Q)) [*] b) : b in X },Q)) [= ( Bottom Q) by LATTICE3:def 21;

      then (( "/\" ({ ( Bottom a) : a in X },Q)) [*] ( "\/" (X,Q))) [= ( Bottom Q) by Def5;

      then

       A2: ( "/\" ({ ( Bottom a) : a in X },Q)) [= ( Bottom ( "\/" (X,Q))) by Th12;

      ( Bottom ( "\/" (X,Q))) is_less_than { ( Bottom a) : a in X }

      proof

        let b;

        assume b in { ( Bottom a) : a in X };

        then

        consider a such that

         A3: b = ( Bottom a) and

         A4: a in X;

        a [= ( "\/" (X,Q)) by A4, LATTICE3: 38;

        hence thesis by A3, Th13;

      end;

      then ( Bottom ( "\/" (X,Q))) [= ( "/\" ({ ( Bottom a) : a in X },Q)) by LATTICE3: 39;

      hence thesis by A2, LATTICES: 8;

    end;

    theorem :: QUANTAL1:25



     Th25: ( Bottom ( "/\" (X,Q))) = ( "\/" ({ ( Bottom a) : a in X },Q))

    proof

      X is_greater_than ( "/\" ({ ( Bottom a) : a in { ( Bottom b) : b in X } },Q))

      proof

        let c;

        assume c in X;

        then ( Bottom c) in { ( Bottom b) : b in X };

        then

         A1: ( Bottom ( Bottom c)) in { ( Bottom a) : a in { ( Bottom b) : b in X } };

        ( Bottom ( Bottom c)) = c by Th22;

        hence thesis by A1, LATTICE3: 38;

      end;

      then

       A2: ( "/\" ({ ( Bottom a) : a in { ( Bottom b) : b in X } },Q)) [= ( "/\" (X,Q)) by LATTICE3: 39;

      { ( Bottom a) : a in { ( Bottom b) : b in X } } c= X

      proof

        let x be object;

        assume x in { ( Bottom a) : a in { ( Bottom b) : b in X } };

        then

        consider a such that

         A3: x = ( Bottom a) & a in { ( Bottom b) : b in X };

        ex b st a = ( Bottom b) & b in X by A3;

        hence thesis by A3, Th22;

      end;

      then ( "/\" (X,Q)) [= ( "/\" ({ ( Bottom a) : a in { ( Bottom b) : b in X } },Q)) by LATTICE3: 45;

      then ( "/\" (X,Q)) = ( "/\" ({ ( Bottom a) : a in { ( Bottom b) : b in X } },Q)) by A2, LATTICES: 8;



      hence ( Bottom ( "/\" (X,Q))) = ( Bottom ( Bottom ( "\/" ({ ( Bottom a) : a in X },Q)))) by Th24

      .= ( "\/" ({ ( Bottom a) : a in X },Q)) by Th22;

    end;

    theorem :: QUANTAL1:26



     Th26: ( Bottom (a "\/" b)) = (( Bottom a) "/\" ( Bottom b)) & ( Bottom (a "/\" b)) = (( Bottom a) "\/" ( Bottom b))

    proof



       A1: { ( Bottom c) : c in {a, b} } = {( Bottom a), ( Bottom b)}

      proof

        thus { ( Bottom c) : c in {a, b} } c= {( Bottom a), ( Bottom b)}

        proof

          let x be object;

          assume x in { ( Bottom c) : c in {a, b} };

          then

          consider c such that

           A2: x = ( Bottom c) and

           A3: c in {a, b};

          c = a or c = b by A3, TARSKI:def 2;

          hence thesis by A2, TARSKI:def 2;

        end;

        let x be object;

        assume x in {( Bottom a), ( Bottom b)};

        then x = ( Bottom a) & a in {a, b} or x = ( Bottom b) & b in {a, b} by TARSKI:def 2;

        hence thesis;

      end;

      (a "\/" b) = ( "\/" {a, b}) & (( Bottom a) "/\" ( Bottom b)) = ( "/\" {( Bottom a), ( Bottom b)}) by LATTICE3: 43;

      hence ( Bottom (a "\/" b)) = (( Bottom a) "/\" ( Bottom b)) by A1, Th24;

      (( Bottom a) "\/" ( Bottom b)) = ( "\/" {( Bottom a), ( Bottom b)}) & (a "/\" b) = ( "/\" {a, b}) by LATTICE3: 43;

      hence thesis by A1, Th25;

    end;

    definition

      let Q, a, b;

      :: QUANTAL1:def27

      func a delta b -> Element of Q equals ( Bottom (( Bottom a) [*] ( Bottom b)));

      correctness ;

    end

    theorem :: QUANTAL1:27

    (a [*] ( "\/" (X,Q))) = ( "\/" ({ (a [*] b) : b in X },Q)) & (a delta ( "/\" (X,Q))) = ( "/\" ({ (a delta c) : c in X },Q))

    proof

      deffunc F( Element of Q) = (( Bottom a) [*] $1);

      deffunc G( Element of Q) = ( Bottom $1);

      deffunc H( Element of Q) = (( Bottom a) [*] ( Bottom $1));

      defpred P[ set] means $1 in X;

      deffunc F1( Element of Q) = ( Bottom (( Bottom a) [*] ( Bottom $1)));

      deffunc F2( Element of Q) = (a delta $1);

      thus (a [*] ( "\/" (X,Q))) = ( "\/" ({ (a [*] b) : b in X },Q)) by Def5;



       A1: { F(c) : c in { G(d) : P[d] } } = { F(G) : P[b] } from DenestFraenkel;



       A2: { G(c) : c in { H(d) : P[d] } } = { G(H) : P[b] } from DenestFraenkel;



       A3: F1(b) = F2(b);



       A4: { F1(b) : P[b] } = { F2(c) : P[c] } from FRAENKEL:sch 5( A3);



      thus (a delta ( "/\" (X,Q))) = ( Bottom (( Bottom a) [*] ( "\/" ({ ( Bottom b) : b in X },Q)))) by Th25

      .= ( Bottom ( "\/" ({ (( Bottom a) [*] ( Bottom b)) : b in X },Q))) by A1, Def5

      .= ( "/\" ({ (a delta b) : b in X },Q)) by A2, A4, Th24;

    end;

    theorem :: QUANTAL1:28

    (( "\/" (X,Q)) [*] a) = ( "\/" ({ (b [*] a) : b in X },Q)) & (( "/\" (X,Q)) delta a) = ( "/\" ({ (c delta a) : c in X },Q))

    proof

      deffunc F( Element of Q) = ($1 [*] ( Bottom a));

      deffunc G( Element of Q) = ( Bottom $1);

      deffunc H( Element of Q) = (( Bottom $1) [*] ( Bottom a));

      defpred P[ set] means $1 in X;

      deffunc F1( Element of Q) = ( Bottom (( Bottom $1) [*] ( Bottom a)));

      deffunc F2( Element of Q) = ($1 delta a);

      thus (( "\/" (X,Q)) [*] a) = ( "\/" ({ (b [*] a) : b in X },Q)) by Def6;



       A1: { F(c) : c in { G(d) : P[d] } } = { F(G) : P[b] } from DenestFraenkel;



       A2: { G(c) : c in { H(d) : P[d] } } = { G(H) : P[b] } from DenestFraenkel;



       A3: F1(b) = F2(b);



       A4: { F1(b) : P[b] } = { F2(c) : P[c] } from FRAENKEL:sch 5( A3);



      thus (( "/\" (X,Q)) delta a) = ( Bottom (( "\/" ({ ( Bottom b) : b in X },Q)) [*] ( Bottom a))) by Th25

      .= ( Bottom ( "\/" ({ (( Bottom b) [*] ( Bottom a)) : b in X },Q))) by A1, Def6

      .= ( "/\" ({ (b delta a) : b in X },Q)) by A2, A4, Th24;

    end;

    theorem :: QUANTAL1:29

    (a delta (b "/\" c)) = ((a delta b) "/\" (a delta c)) & ((b "/\" c) delta a) = ((b delta a) "/\" (c delta a))

    proof



      thus (a delta (b "/\" c)) = ( Bottom (( Bottom a) [*] (( Bottom b) "\/" ( Bottom c)))) by Th26

      .= ( Bottom ((( Bottom a) [*] ( Bottom b)) "\/" (( Bottom a) [*] ( Bottom c)))) by Th6

      .= ((a delta b) "/\" (a delta c)) by Th26;



      thus ((b "/\" c) delta a) = ( Bottom ((( Bottom b) "\/" ( Bottom c)) [*] ( Bottom a))) by Th26

      .= ( Bottom ((( Bottom b) [*] ( Bottom a)) "\/" (( Bottom c) [*] ( Bottom a)))) by Th6

      .= ((b delta a) "/\" (c delta a)) by Th26;

    end;

    theorem :: QUANTAL1:30

    a1 [= b1 & a2 [= b2 implies (a1 delta a2) [= (b1 delta b2)

    proof

      assume a1 [= b1 & a2 [= b2;

      then ( Bottom b1) [= ( Bottom a1) & ( Bottom b2) [= ( Bottom a2) by Th13;

      then (( Bottom b1) [*] ( Bottom b2)) [= (( Bottom a1) [*] ( Bottom a2)) by Th9;

      hence thesis by Th13;

    end;

    theorem :: QUANTAL1:31

    ((a delta b) delta c) = (a delta (b delta c))

    proof



      thus ((a delta b) delta c) = ( Bottom ((( Bottom a) [*] ( Bottom b)) [*] ( Bottom c))) by Th22

      .= ( Bottom (( Bottom a) [*] (( Bottom b) [*] ( Bottom c)))) by GROUP_1:def 3

      .= (a delta (b delta c)) by Th22;

    end;

    theorem :: QUANTAL1:32



     Th32: (a [*] ( Top Q)) = a & (( Top Q) [*] a) = a

    proof

      the absurd of Q is dualizing by Def20;

      then

       A1: ( Top Q) = ( the_unity_wrt times(Q)) by Th19;

       times(Q) is having_a_unity by MONOID_0:def 10;

      hence thesis by A1, SETWISEO: 15;

    end;

    theorem :: QUANTAL1:33

    (a delta ( Bottom Q)) = a & (( Bottom Q) delta a) = a

    proof

      (( Bottom a) [*] ( Top Q)) = ( Bottom a) & (( Top Q) [*] ( Bottom a)) = ( Bottom a) by Th32;

      hence thesis by Th22;

    end;

    theorem :: QUANTAL1:34

    for Q be Quantale holds for j be UnOp of Q st j is monotone idempotent \/-distributive holds ex L be complete Lattice st the carrier of L = ( rng j) & for X be Subset of L holds ( "\/" X) = (j . ( "\/" (X,Q)))

    proof

      let Q be Quantale, j be UnOp of Q;

      assume

       A1: j is monotone idempotent \/-distributive;

      reconsider D = ( rng j) as non empty Subset of Q;

      ( dom j) = carr(Q) by FUNCT_2:def 1;

      then

      reconsider j9 = j as Function of carr(Q), D by RELSET_1: 4;

      deffunc F( Subset of D) = (j9 . ( "\/" ($1,Q)));

      consider f be Function of ( bool D), D such that

       A2: for X be Subset of D holds (f . X) = F(X) from FUNCT_2:sch 4;



       A3: ( dom f) = ( bool D) by FUNCT_2:def 1;



       A4: for X be Subset-Family of D holds (f . (f .: X)) = (f . ( union X))

      proof

        let X be Subset-Family of D;

        set A = { (j . a) where a be Element of Q : a in (f .: X) };

        set B = { (j . b) where b be Element of Q : b in ( union X) };

        reconsider Y = (f .: X), X9 = ( union X) as Subset of Q by XBOOLE_1: 1;

        now

          let a be Element of Q;

          assume a in B;

          then

          consider b9 be Element of Q such that

           A5: a = (j . b9) and

           A6: b9 in ( union X);

          consider Y be set such that

           A7: b9 in Y and

           A8: Y in X by A6, TARSKI:def 4;

          reconsider Y as Subset of D by A8;



           A9: b9 [= ( "\/" (Y,Q)) by A7, LATTICE3: 38;

          take b = (j . ( "\/" (Y,Q)));

          b = (f . Y) by A2;

          then

           A10: b in (f .: X) by A3, A8, FUNCT_1:def 6;

          (j . b) = b by A1, Lm1;

          hence a [= b & b in A by A1, A5, A10, A9;

        end;

        then

         A11: ( "\/" (B,Q)) [= ( "\/" (A,Q)) by LATTICE3: 47;

        A is_less_than ( "\/" (B,Q))

        proof

          let a be Element of Q;

          assume a in A;

          then

          consider a9 be Element of Q such that

           A12: a = (j . a9) and

           A13: a9 in (f .: X);

          consider x be object such that

           A14: x in ( dom f) and

           A15: x in X and

           A16: a9 = (f . x) by A13, FUNCT_1:def 6;

          reconsider x as Subset of D by A14;

          reconsider Y = x as Subset of Q by XBOOLE_1: 1;



           A17: { (j . b) where b be Element of Q : b in Y } c= B

          proof

            let z be object;

            assume z in { (j . b) where b be Element of Q : b in Y };

            then

            consider b be Element of Q such that

             A18: z = (j . b) and

             A19: b in Y;

            b in ( union X) by A15, A19, TARSKI:def 4;

            hence thesis by A18;

          end;

          a9 = (j . ( "\/" Y)) by A2, A16;

          then a9 = ( "\/" ({ (j . b) where b be Element of Q : b in Y },Q)) by A1, Th10;

          then a9 [= ( "\/" (B,Q)) by A17, LATTICE3: 45;

          then a [= (j . ( "\/" (B,Q))) by A1, A12;

          then a [= (j . (j . ( "\/" X9))) by A1, Th10;

          then a [= (j . ( "\/" X9)) by A1, Lm1;

          hence thesis by A1, Th10;

        end;

        then

         A20: ( "\/" (A,Q)) [= ( "\/" (B,Q)) by LATTICE3:def 21;



        thus (f . (f .: X)) = (j . ( "\/" Y)) by A2

        .= ( "\/" (A,Q)) by A1, Th10

        .= ( "\/" (B,Q)) by A20, A11, LATTICES: 8

        .= (j . ( "\/" X9)) by A1, Th10

        .= (f . ( union X)) by A2;

      end;

      for a be Element of D holds (f . {a}) = a

      proof

        let a be Element of D;

        consider a9 be object such that

         A21: a9 in ( dom j) and

         A22: a = (j . a9) by FUNCT_1:def 3;

        reconsider x = a as Element of Q;

        reconsider x9 = {x} as Subset of Q;

        reconsider a9 as Element of Q by A21;



        thus (f . {a}) = (j . ( "\/" x9)) by A2

        .= (j . (j . a9)) by A22, LATTICE3: 42

        .= a by A1, A22, Lm1;

      end;

      then

      consider L be complete strict Lattice such that

       A23: carr(L) = D and

       A24: for X be Subset of L holds ( "\/" X) = (f . X) by A4, LATTICE3: 55;

      take L;

      thus carr(L) = ( rng j) by A23;

      let X be Subset of L;



      thus ( "\/" X) = (f . X) by A24

      .= (j . ( "\/" (X,Q))) by A2, A23;

    end;