:: QUANTAL1 semantic presentation begin scheme :: QUANTAL1:sch 1 DenestFraenkel{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> set , F4( set ) -> Element of F2(), P1[ set ] } : { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } = { F3(F4(a)) where a is Element of F1() : P1[a] } proof thus { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } c= { F3(F4(a)) where a is Element of F1() : P1[a] } :: according to XBOOLE_0:def_10 ::_thesis: { F3(F4(a)) where a is Element of F1() : P1[a] } c= { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } or x in { F3(F4(a)) where a is Element of F1() : P1[a] } ) assume x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } ; ::_thesis: x in { F3(F4(a)) where a is Element of F1() : P1[a] } then consider a being Element of F2() such that A1: x = F3(a) and A2: a in { F4(b) where b is Element of F1() : P1[b] } ; ex b being Element of F1() st ( a = F4(b) & P1[b] ) by A2; hence x in { F3(F4(a)) where a is Element of F1() : P1[a] } by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(F4(a)) where a is Element of F1() : P1[a] } or x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } ) assume x in { F3(F4(a)) where a is Element of F1() : P1[a] } ; ::_thesis: x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } then consider a being Element of F1() such that A3: x = F3(F4(a)) and A4: P1[a] ; F4(a) in { F4(b) where b is Element of F1() : P1[b] } by A4; hence x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } by A3; ::_thesis: verum end; scheme :: QUANTAL1:sch 2 EmptyFraenkel{ F1() -> non empty set , F2( set ) -> set , P1[ set ] } : { F2(a) where a is Element of F1() : P1[a] } = {} provided A1: for a being Element of F1() holds P1[a] proof assume not { F2(a) where a is Element of F1() : P1[a] } = {} ; ::_thesis: contradiction then reconsider X = { F2(a) where a is Element of F1() : P1[a] } as non empty set ; set x = the Element of X; the Element of X in X ; then ex a being Element of F1() st ( the Element of X = F2(a) & P1[a] ) ; hence contradiction by A1; ::_thesis: verum end; deffunc H1( non empty LattStr ) -> set = the carrier of \$1; deffunc H2( LattStr ) -> Element of bool [:[: the carrier of \$1, the carrier of \$1:], the carrier of \$1:] = the L_join of \$1; deffunc H3( LattStr ) -> Element of bool [:[: the carrier of \$1, the carrier of \$1:], the carrier of \$1:] = the L_meet of \$1; deffunc H4( multMagma ) -> Element of bool [:[: the carrier of \$1, the carrier of \$1:], the carrier of \$1:] = the multF of \$1; theorem Th1: :: QUANTAL1:1 for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) proof let L1, L2 be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) let a1, b1 be Element of L1; ::_thesis: for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) let a2, b2 be Element of L2; ::_thesis: ( a1 = a2 & b1 = b2 implies ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) ) assume A2: ( a1 = a2 & b1 = b2 ) ; ::_thesis: ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) thus a1 "\/" b1 = a2 "\/" b2 by A1, A2; ::_thesis: ( a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) thus a1 "/\" b1 = a2 "/\" b2 by A1, A2; ::_thesis: ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) A3: ( a2 "\/" b2 = b2 iff a2 [= b2 ) by LATTICES:def_3; ( a1 [= b1 iff a1 "\/" b1 = b1 ) by LATTICES:def_3; hence ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) by A1, A2, A3; ::_thesis: verum end; theorem Th2: :: QUANTAL1:2 for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds for a being Element of L1 for b being Element of L2 for X being set st a = b holds ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) proof let L1, L2 be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a being Element of L1 for b being Element of L2 for X being set st a = b holds ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for a being Element of L1 for b being Element of L2 for X being set st a = b holds ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) let a be Element of L1; ::_thesis: for b being Element of L2 for X being set st a = b holds ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) let b be Element of L2; ::_thesis: for X being set st a = b holds ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) let X be set ; ::_thesis: ( a = b implies ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) ) assume A2: a = b ; ::_thesis: ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) thus ( a is_less_than X implies b is_less_than X ) ::_thesis: ( ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) proof assume A3: for c being Element of L1 st c in X holds a [= c ; :: according to LATTICE3:def_16 ::_thesis: b is_less_than X let c be Element of L2; :: according to LATTICE3:def_16 ::_thesis: ( not c in X or b [= c ) reconsider d = c as Element of L1 by A1; assume c in X ; ::_thesis: b [= c then a [= d by A3; hence b [= c by A1, A2, Th1; ::_thesis: verum end; thus ( b is_less_than X implies a is_less_than X ) ::_thesis: ( a is_greater_than X iff b is_greater_than X ) proof assume A4: for c being Element of L2 st c in X holds b [= c ; :: according to LATTICE3:def_16 ::_thesis: a is_less_than X let c be Element of L1; :: according to LATTICE3:def_16 ::_thesis: ( not c in X or a [= c ) reconsider d = c as Element of L2 by A1; assume c in X ; ::_thesis: a [= c then b [= d by A4; hence a [= c by A1, A2, Th1; ::_thesis: verum end; thus ( a is_greater_than X implies b is_greater_than X ) ::_thesis: ( b is_greater_than X implies a is_greater_than X ) proof assume A5: for c being Element of L1 st c in X holds c [= a ; :: according to LATTICE3:def_17 ::_thesis: b is_greater_than X let c be Element of L2; :: according to LATTICE3:def_17 ::_thesis: ( not c in X or c [= b ) reconsider d = c as Element of L1 by A1; assume c in X ; ::_thesis: c [= b then d [= a by A5; hence c [= b by A1, A2, Th1; ::_thesis: verum end; assume A6: for c being Element of L2 st c in X holds c [= b ; :: according to LATTICE3:def_17 ::_thesis: a is_greater_than X let c be Element of L1; :: according to LATTICE3:def_17 ::_thesis: ( not c in X or c [= a ) reconsider d = c as Element of L2 by A1; assume c in X ; ::_thesis: c [= a then d [= b by A6; hence c [= a by A1, A2, Th1; ::_thesis: verum end; definition let L be 1-sorted ; mode UnOp of L is Function of L,L; end; definition let L be non empty LattStr ; let X be Subset of L; attrX is directed means :: QUANTAL1:def 1 for Y being finite Subset of X ex x being Element of L st ( "\/" (Y,L) [= x & x in X ); end; :: deftheorem defines directed QUANTAL1:def_1_:_ for L being non empty LattStr for X being Subset of L holds ( X is directed iff for Y being finite Subset of X ex x being Element of L st ( "\/" (Y,L) [= x & x in X ) ); theorem :: QUANTAL1:3 for L being non empty LattStr for X being Subset of L st X is directed holds not X is empty proof let L be non empty LattStr ; ::_thesis: for X being Subset of L st X is directed holds not X is empty let X be Subset of L; ::_thesis: ( X is directed implies not X is empty ) assume for Y being finite Subset of X ex x being Element of L st ( "\/" (Y,L) [= x & x in X ) ; :: according to QUANTAL1:def_1 ::_thesis: not X is empty then ex x being Element of L st ( "\/" (({} X),L) [= x & x in X ) ; hence not X is empty ; ::_thesis: verum end; definition attrc1 is strict ; struct QuantaleStr -> LattStr , multMagma ; aggrQuantaleStr(# carrier, L_join, L_meet, multF #) -> QuantaleStr ; end; registration cluster non empty for QuantaleStr ; existence not for b1 being QuantaleStr holds b1 is empty proof set A = the non empty set ; set b1 = the BinOp of the non empty set ; take QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) ; ::_thesis: not QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) is empty thus not the carrier of QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; definition attrc1 is strict ; struct QuasiNetStr -> QuantaleStr , multLoopStr ; aggrQuasiNetStr(# carrier, L_join, L_meet, multF, OneF #) -> QuasiNetStr ; end; registration cluster non empty for QuasiNetStr ; existence not for b1 being QuasiNetStr holds b1 is empty proof set A = the non empty set ; set b1 = the BinOp of the non empty set ; set e = the Element of the non empty set ; take QuasiNetStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) ; ::_thesis: not QuasiNetStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty thus not the carrier of QuasiNetStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; definition let IT be non empty multMagma ; attrIT is with_left-zero means :: QUANTAL1:def 2 ex a being Element of IT st for b being Element of IT holds a * b = a; attrIT is with_right-zero means :: QUANTAL1:def 3 ex b being Element of IT st for a being Element of IT holds a * b = b; end; :: deftheorem defines with_left-zero QUANTAL1:def_2_:_ for IT being non empty multMagma holds ( IT is with_left-zero iff ex a being Element of IT st for b being Element of IT holds a * b = a ); :: deftheorem defines with_right-zero QUANTAL1:def_3_:_ for IT being non empty multMagma holds ( IT is with_right-zero iff ex b being Element of IT st for a being Element of IT holds a * b = b ); definition let IT be non empty multMagma ; attrIT is with_zero means :Def4: :: QUANTAL1:def 4 ( IT is with_left-zero & IT is with_right-zero ); end; :: deftheorem Def4 defines with_zero QUANTAL1:def_4_:_ for IT being non empty multMagma holds ( IT is with_zero iff ( IT is with_left-zero & IT is with_right-zero ) ); registration cluster non empty with_zero -> non empty with_left-zero with_right-zero for multMagma ; coherence for b1 being non empty multMagma st b1 is with_zero holds ( b1 is with_left-zero & b1 is with_right-zero ) by Def4; cluster non empty with_left-zero with_right-zero -> non empty with_zero for multMagma ; coherence for b1 being non empty multMagma st b1 is with_left-zero & b1 is with_right-zero holds b1 is with_zero by Def4; end; registration cluster non empty with_zero for multMagma ; existence ex b1 being non empty multMagma st b1 is with_zero proof set x = the set ; set f = the BinOp of { the set }; take G = multMagma(# { the set }, the BinOp of { the set } #); ::_thesis: G is with_zero reconsider x = the set as Element of G by TARSKI:def_1; thus G is with_left-zero :: according to QUANTAL1:def_4 ::_thesis: G is with_right-zero proof take x ; :: according to QUANTAL1:def_2 ::_thesis: for b being Element of G holds x * b = x thus for b being Element of G holds x * b = x by TARSKI:def_1; ::_thesis: verum end; take x ; :: according to QUANTAL1:def_3 ::_thesis: for a being Element of G holds a * x = x thus for a being Element of G holds a * x = x by TARSKI:def_1; ::_thesis: verum end; end; definition let IT be non empty QuantaleStr ; attrIT is right-distributive means :Def5: :: QUANTAL1:def 5 for a being Element of IT for X being set holds a [*] ("\/" (X,IT)) = "\/" ( { (a [*] b) where b is Element of IT : b in X } ,IT); attrIT is left-distributive means :Def6: :: QUANTAL1:def 6 for a being Element of IT for X being set holds ("\/" (X,IT)) [*] a = "\/" ( { (b [*] a) where b is Element of IT : b in X } ,IT); attrIT is times-additive means :: QUANTAL1:def 7 for a, b, c being Element of IT holds ( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ); attrIT is times-continuous means :: QUANTAL1:def 8 for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds ("\/" X1) [*] ("\/" X2) = "\/" ( { (a [*] b) where a, b is Element of IT : ( a in X1 & b in X2 ) } ,IT); end; :: deftheorem Def5 defines right-distributive QUANTAL1:def_5_:_ for IT being non empty QuantaleStr holds ( IT is right-distributive iff for a being Element of IT for X being set holds a [*] ("\/" (X,IT)) = "\/" ( { (a [*] b) where b is Element of IT : b in X } ,IT) ); :: deftheorem Def6 defines left-distributive QUANTAL1:def_6_:_ for IT being non empty QuantaleStr holds ( IT is left-distributive iff for a being Element of IT for X being set holds ("\/" (X,IT)) [*] a = "\/" ( { (b [*] a) where b is Element of IT : b in X } ,IT) ); :: deftheorem defines times-additive QUANTAL1:def_7_:_ for IT being non empty QuantaleStr holds ( IT is times-additive iff for a, b, c being Element of IT holds ( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) ); :: deftheorem defines times-continuous QUANTAL1:def_8_:_ for IT being non empty QuantaleStr holds ( IT is times-continuous iff for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds ("\/" X1) [*] ("\/" X2) = "\/" ( { (a [*] b) where a, b is Element of IT : ( a in X1 & b in X2 ) } ,IT) ); theorem Th4: :: QUANTAL1:4 for Q being non empty QuantaleStr st LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} holds ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like ) proof set B = BooleLatt {}; let Q be non empty QuantaleStr ; ::_thesis: ( LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} implies ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like ) ) set a = the Element of Q; assume A1: LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} ; ::_thesis: ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like ) A2: now__::_thesis:_for_x,_y_being_Element_of_Q_holds_x_=_y let x, y be Element of Q; ::_thesis: x = y A3: H1( BooleLatt {}) = {{}} by LATTICE3:def_1, ZFMISC_1:1; then x = {} by A1, TARSKI:def_1; hence x = y by A1, A3, TARSKI:def_1; ::_thesis: verum end; thus H4(Q) is associative :: according to MONOID_0:def_12 ::_thesis: ( Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like ) proof let a, b, c be Element of Q; :: according to BINOP_1:def_3 ::_thesis: H4(Q) . (a,(H4(Q) . (b,c))) = H4(Q) . ((H4(Q) . (a,b)),c) thus H4(Q) . (a,(H4(Q) . (b,c))) = H4(Q) . ((H4(Q) . (a,b)),c) by A2; ::_thesis: verum end; A4: ( ( for p, q, r being Element of Q holds p "/\" (q "/\" r) = (p "/\" q) "/\" r ) & ( for p, q being Element of Q holds p "/\" (p "\/" q) = p ) ) by A2; thus H4(Q) is commutative :: according to MONOID_0:def_11 ::_thesis: ( Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like ) proof let a, b be Element of Q; :: according to BINOP_1:def_2 ::_thesis: H4(Q) . (a,b) = H4(Q) . (b,a) thus H4(Q) . (a,b) = H4(Q) . (b,a) by A2; ::_thesis: verum end; thus H4(Q) is having_a_unity :: according to MONOID_0:def_10 ::_thesis: ( Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like ) proof take the Element of Q ; :: according to SETWISEO:def_2 ::_thesis: the Element of Q is_a_unity_wrt H4(Q) thus the Element of Q is_a_left_unity_wrt H4(Q) :: according to BINOP_1:def_7 ::_thesis: the Element of Q is_a_right_unity_wrt H4(Q) proof let b be Element of Q; :: according to BINOP_1:def_16 ::_thesis: H4(Q) . ( the Element of Q,b) = b thus H4(Q) . ( the Element of Q,b) = b by A2; ::_thesis: verum end; let b be Element of Q; :: according to BINOP_1:def_17 ::_thesis: H4(Q) . (b, the Element of Q) = b thus H4(Q) . (b, the Element of Q) = b by A2; ::_thesis: verum end; thus Q is with_zero ::_thesis: ( Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like ) proof thus Q is with_left-zero :: according to QUANTAL1:def_4 ::_thesis: Q is with_right-zero proof take the Element of Q ; :: according to QUANTAL1:def_2 ::_thesis: for b being Element of Q holds the Element of Q * b = the Element of Q thus for b being Element of Q holds the Element of Q * b = the Element of Q by A2; ::_thesis: verum end; take the Element of Q ; :: according to QUANTAL1:def_3 ::_thesis: for a being Element of Q holds a * the Element of Q = the Element of Q thus for a being Element of Q holds a * the Element of Q = the Element of Q by A2; ::_thesis: verum end; now__::_thesis:_for_X_being_set_ex_p9_being_Element_of_Q_st_ (_X_is_less_than_p9_&_(_for_r9_being_Element_of_Q_st_X_is_less_than_r9_holds_ p9_[=_r9_)_) let X be set ; ::_thesis: ex p9 being Element of Q st ( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds p9 [= r9 ) ) consider p being Element of (BooleLatt {}) such that A5: X is_less_than p and A6: for r being Element of (BooleLatt {}) st X is_less_than r holds p [= r by LATTICE3:def_18; reconsider p9 = p as Element of Q by A1; take p9 = p9; ::_thesis: ( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds p9 [= r9 ) ) thus X is_less_than p9 by A1, A5, Th2; ::_thesis: for r9 being Element of Q st X is_less_than r9 holds p9 [= r9 let r9 be Element of Q; ::_thesis: ( X is_less_than r9 implies p9 [= r9 ) reconsider r = r9 as Element of (BooleLatt {}) by A1; assume X is_less_than r9 ; ::_thesis: p9 [= r9 then X is_less_than r by A1, Th2; then p [= r by A6; hence p9 [= r9 by A1, Th1; ::_thesis: verum end; hence for X being set ex p being Element of Q st ( X is_less_than p & ( for r being Element of Q st X is_less_than r holds p [= r ) ) ; :: according to LATTICE3:def_18 ::_thesis: ( Q is right-distributive & Q is left-distributive & Q is Lattice-like ) thus Q is right-distributive ::_thesis: ( Q is left-distributive & Q is Lattice-like ) proof let a be Element of Q; :: according to QUANTAL1:def_5 ::_thesis: for X being set holds a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) let X be set ; ::_thesis: a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) thus a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) by A2; ::_thesis: verum end; thus Q is left-distributive ::_thesis: Q is Lattice-like proof let a be Element of Q; :: according to QUANTAL1:def_6 ::_thesis: for X being set holds ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) let X be set ; ::_thesis: ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) thus ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) by A2; ::_thesis: verum end; A7: ( ( for p, q being Element of Q holds (p "/\" q) "\/" q = q ) & ( for p, q being Element of Q holds p "/\" q = q "/\" p ) ) by A2; ( ( for p, q being Element of Q holds p "\/" q = q "\/" p ) & ( for p, q, r being Element of Q holds p "\/" (q "\/" r) = (p "\/" q) "\/" r ) ) by A2; then ( Q is join-commutative & Q is join-associative & Q is meet-absorbing & Q is meet-commutative & Q is meet-associative & Q is join-absorbing ) by A7, A4, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; hence Q is Lattice-like ; ::_thesis: verum end; registration let A be non empty set ; let b1, b2, b3 be BinOp of A; cluster QuantaleStr(# A,b1,b2,b3 #) -> non empty ; coherence not QuantaleStr(# A,b1,b2,b3 #) is empty ; end; registration cluster non empty unital associative commutative Lattice-like complete with_zero right-distributive left-distributive for QuantaleStr ; existence ex b1 being non empty QuantaleStr st ( b1 is associative & b1 is commutative & b1 is unital & b1 is with_zero & b1 is left-distributive & b1 is right-distributive & b1 is complete & b1 is Lattice-like ) proof set B = BooleLatt {}; set b = the BinOp of (BooleLatt {}); take QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) ; ::_thesis: ( QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is associative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is commutative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is unital & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is with_zero & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is left-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is right-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is complete & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is Lattice-like ) thus ( QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is associative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is commutative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is unital & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is with_zero & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is left-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is right-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is complete & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is Lattice-like ) by Th4; ::_thesis: verum end; end; scheme :: QUANTAL1:sch 3 LUBFraenkelDistr{ F1() -> non empty Lattice-like complete QuantaleStr , F2( set , set ) -> Element of F1(), F3() -> set , F4() -> set } : "\/" ( { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ,F1()) = "\/" ( { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ,F1()) proof set Q = F1(); set X = F3(); set Y = F4(); set Z = { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ; set W = { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } ; set S = { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ; A1: { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } = { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } proof thus { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } c= { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } :: according to XBOOLE_0:def_10 ::_thesis: { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } c= { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } or x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ) assume x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } ; ::_thesis: x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } then consider V being Subset of F1() such that A2: x = "\/" V and A3: V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ; ex a being Element of F1() st ( V = { F2(a,b) where b is Element of F1() : b in F4() } & a in F3() ) by A3; hence x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } or x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } ) assume x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ; ::_thesis: x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } then consider a being Element of F1() such that A4: x = "\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1()) and A5: a in F3() ; A6: { F2(a,b) where b is Element of F1() : b in F4() } c= H1(F1()) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { F2(a,b) where b is Element of F1() : b in F4() } or y in H1(F1()) ) assume y in { F2(a,b) where b is Element of F1() : b in F4() } ; ::_thesis: y in H1(F1()) then ex b being Element of F1() st ( y = F2(a,b) & b in F4() ) ; hence y in H1(F1()) ; ::_thesis: verum end; { F2(a,c) where c is Element of F1() : c in F4() } in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by A5; hence x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } by A4, A6; ::_thesis: verum end; A7: { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } = union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } proof thus { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } c= union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } :: according to XBOOLE_0:def_10 ::_thesis: union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } c= { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } or x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ) assume x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ; ::_thesis: x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } then consider a, b being Element of F1() such that A8: ( x = F2(a,b) & a in F3() & b in F4() ) ; ( x in { F2(a,c) where c is Element of F1() : c in F4() } & { F2(a,d) where d is Element of F1() : d in F4() } in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ) by A8; hence x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } or x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ) assume x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ; ::_thesis: x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } then consider V being set such that A9: x in V and A10: V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by TARSKI:def_4; consider a being Element of F1() such that A11: V = { F2(a,b) where b is Element of F1() : b in F4() } and A12: a in F3() by A10; ex b being Element of F1() st ( x = F2(a,b) & b in F4() ) by A9, A11; hence x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } by A12; ::_thesis: verum end; { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } c= bool H1(F1()) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } or x in bool H1(F1()) ) assume x in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ; ::_thesis: x in bool H1(F1()) then consider a being Element of F1() such that A13: x = { F2(a,b) where b is Element of F1() : b in F4() } and a in F3() ; x c= H1(F1()) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in H1(F1()) ) assume y in x ; ::_thesis: y in H1(F1()) then ex b being Element of F1() st ( y = F2(a,b) & b in F4() ) by A13; hence y in H1(F1()) ; ::_thesis: verum end; hence x in bool H1(F1()) ; ::_thesis: verum end; hence "\/" ( { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ,F1()) = "\/" ( { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ,F1()) by A1, A7, LATTICE3:48; ::_thesis: verum end; theorem Th5: :: QUANTAL1:5 for Q being non empty Lattice-like complete right-distributive left-distributive QuantaleStr for X, Y being set holds ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q) proof let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; ::_thesis: for X, Y being set holds ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q) let X, Y be set ; ::_thesis: ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q) deffunc H5( Element of Q) -> Element of the carrier of Q = \$1 [*] ("\/" (Y,Q)); deffunc H6( Element of Q) -> Element of the carrier of Q = "\/" ( { (\$1 [*] b) where b is Element of Q : b in Y } ,Q); defpred S1[ set ] means \$1 in X; deffunc H7( Element of Q, Element of Q) -> Element of the carrier of Q = \$1 [*] \$2; A1: for a being Element of Q holds H5(a) = H6(a) by Def5; { H5(c) where c is Element of Q : S1[c] } = { H6(a) where a is Element of Q : S1[a] } from FRAENKEL:sch_5(A1); hence ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { ("\/" ( { H7(a,b) where b is Element of Q : b in Y } ,Q)) where a is Element of Q : a in X } ,Q) by Def6 .= "\/" ( { H7(c,d) where c, d is Element of Q : ( c in X & d in Y ) } ,Q) from QUANTAL1:sch_3() ; ::_thesis: verum end; theorem Th6: :: QUANTAL1:6 for Q being non empty Lattice-like complete right-distributive left-distributive QuantaleStr for a, b, c being Element of Q holds ( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) proof let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; ::_thesis: for a, b, c being Element of Q holds ( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) let a, b, c be Element of Q; ::_thesis: ( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) set X1 = { (d [*] c) where d is Element of Q : d in {a,b} } ; set X2 = { (c [*] d) where d is Element of Q : d in {a,b} } ; now__::_thesis:_for_x_being_set_holds_ (_(_(_x_=_a_[*]_c_or_x_=_b_[*]_c_)_implies_x_in__{__(d_[*]_c)_where_d_is_Element_of_Q_:_d_in_{a,b}__}__)_&_(_not_x_in__{__(d_[*]_c)_where_d_is_Element_of_Q_:_d_in_{a,b}__}__or_x_=_a_[*]_c_or_x_=_b_[*]_c_)_) let x be set ; ::_thesis: ( ( ( x = a [*] c or x = b [*] c ) implies x in { (d [*] c) where d is Element of Q : d in {a,b} } ) & ( not x in { (d [*] c) where d is Element of Q : d in {a,b} } or x = a [*] c or x = b [*] c ) ) ( a in {a,b} & b in {a,b} ) by TARSKI:def_2; hence ( ( x = a [*] c or x = b [*] c ) implies x in { (d [*] c) where d is Element of Q : d in {a,b} } ) ; ::_thesis: ( not x in { (d [*] c) where d is Element of Q : d in {a,b} } or x = a [*] c or x = b [*] c ) assume x in { (d [*] c) where d is Element of Q : d in {a,b} } ; ::_thesis: ( x = a [*] c or x = b [*] c ) then ex d being Element of Q st ( x = d [*] c & d in {a,b} ) ; hence ( x = a [*] c or x = b [*] c ) by TARSKI:def_2; ::_thesis: verum end; then A1: { (d [*] c) where d is Element of Q : d in {a,b} } = {(a [*] c),(b [*] c)} by TARSKI:def_2; now__::_thesis:_for_x_being_set_holds_ (_(_(_x_=_c_[*]_a_or_x_=_c_[*]_b_)_implies_x_in__{__(c_[*]_d)_where_d_is_Element_of_Q_:_d_in_{a,b}__}__)_&_(_not_x_in__{__(c_[*]_d)_where_d_is_Element_of_Q_:_d_in_{a,b}__}__or_x_=_c_[*]_a_or_x_=_c_[*]_b_)_) let x be set ; ::_thesis: ( ( ( x = c [*] a or x = c [*] b ) implies x in { (c [*] d) where d is Element of Q : d in {a,b} } ) & ( not x in { (c [*] d) where d is Element of Q : d in {a,b} } or x = c [*] a or x = c [*] b ) ) ( a in {a,b} & b in {a,b} ) by TARSKI:def_2; hence ( ( x = c [*] a or x = c [*] b ) implies x in { (c [*] d) where d is Element of Q : d in {a,b} } ) ; ::_thesis: ( not x in { (c [*] d) where d is Element of Q : d in {a,b} } or x = c [*] a or x = c [*] b ) assume x in { (c [*] d) where d is Element of Q : d in {a,b} } ; ::_thesis: ( x = c [*] a or x = c [*] b ) then ex d being Element of Q st ( x = c [*] d & d in {a,b} ) ; hence ( x = c [*] a or x = c [*] b ) by TARSKI:def_2; ::_thesis: verum end; then A2: { (c [*] d) where d is Element of Q : d in {a,b} } = {(c [*] a),(c [*] b)} by TARSKI:def_2; A3: a "\/" b = "\/" {a,b} by LATTICE3:43; then (a "\/" b) [*] c = "\/" ( { (d [*] c) where d is Element of Q : d in {a,b} } ,Q) by Def6; hence (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) by A1, LATTICE3:43; ::_thesis: c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) c [*] (a "\/" b) = "\/" ( { (c [*] d) where d is Element of Q : d in {a,b} } ,Q) by A3, Def5; hence c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) by A2, LATTICE3:43; ::_thesis: verum end; registration let A be non empty set ; let b1, b2, b3 be BinOp of A; let e be Element of A; cluster QuasiNetStr(# A,b1,b2,b3,e #) -> non empty ; coherence not QuasiNetStr(# A,b1,b2,b3,e #) is empty ; end; registration cluster non empty Lattice-like complete for QuasiNetStr ; existence ex b1 being non empty QuasiNetStr st ( b1 is complete & b1 is Lattice-like ) proof set B = BooleLatt {}; set e = the Element of (BooleLatt {}); set b = the BinOp of (BooleLatt {}); take QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) ; ::_thesis: ( QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) is complete & QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) is Lattice-like ) thus ( QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) is complete & QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) is Lattice-like ) by Th4; ::_thesis: verum end; end; registration cluster non empty Lattice-like complete right-distributive left-distributive -> non empty Lattice-like complete times-additive times-continuous for QuasiNetStr ; coherence for b1 being non empty Lattice-like complete QuasiNetStr st b1 is left-distributive & b1 is right-distributive holds ( b1 is times-continuous & b1 is times-additive ) proof let Q be non empty Lattice-like complete QuasiNetStr ; ::_thesis: ( Q is left-distributive & Q is right-distributive implies ( Q is times-continuous & Q is times-additive ) ) assume ( Q is left-distributive & Q is right-distributive ) ; ::_thesis: ( Q is times-continuous & Q is times-additive ) hence ( ( for X, Y being Subset of Q st X is directed & Y is directed holds ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q) ) & ( for a, b, c being Element of Q holds ( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) ) ) by Th5, Th6; :: according to QUANTAL1:def_7,QUANTAL1:def_8 ::_thesis: verum end; end; registration cluster non empty unital associative commutative Lattice-like complete with_left-zero with_zero right-distributive left-distributive for QuasiNetStr ; existence ex b1 being non empty QuasiNetStr st ( b1 is associative & b1 is commutative & b1 is unital & b1 is with_zero & b1 is with_left-zero & b1 is left-distributive & b1 is right-distributive & b1 is complete & b1 is Lattice-like ) proof set B = BooleLatt {}; set e = the Element of (BooleLatt {}); set b = the BinOp of (BooleLatt {}); take Q = QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #); ::_thesis: ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is with_left-zero & Q is left-distributive & Q is right-distributive & Q is complete & Q is Lattice-like ) ( Q is with_zero & Q is unital ) by Th4; hence ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is with_left-zero & Q is left-distributive & Q is right-distributive & Q is complete & Q is Lattice-like ) by Th4; ::_thesis: verum end; end; definition mode Quantale is non empty associative Lattice-like complete right-distributive left-distributive QuantaleStr ; mode QuasiNet is non empty unital associative Lattice-like complete with_left-zero times-additive times-continuous QuasiNetStr ; end; definition mode BlikleNet is with_zero QuasiNet; end; theorem :: QUANTAL1:7 for Q being non empty unital QuasiNetStr st Q is Quantale holds Q is BlikleNet proof defpred S1[ set ] means \$1 in {} ; let Q be non empty unital QuasiNetStr ; ::_thesis: ( Q is Quantale implies Q is BlikleNet ) assume Q is Quantale ; ::_thesis: Q is BlikleNet then reconsider Q9 = Q as Quantale ; A1: Bottom Q9 = "\/" ({},Q9) by LATTICE3:49; A2: for c being Element of Q9 holds not S1[c] ; Q9 is with_zero proof hereby :: according to QUANTAL1:def_2,QUANTAL1:def_4 ::_thesis: Q9 is with_right-zero reconsider a = Bottom Q9 as Element of Q9 ; take a = a; ::_thesis: for b being Element of Q9 holds a [*] b = a let b be Element of Q9; ::_thesis: a [*] b = a deffunc H5( Element of Q9) -> Element of the carrier of Q9 = \$1 [*] b; { H5(c) where c is Element of Q9 : S1[c] } = {} from QUANTAL1:sch_2(A2); hence a [*] b = a by A1, Def6; ::_thesis: verum end; take Bottom Q9 ; :: according to QUANTAL1:def_3 ::_thesis: for a being Element of Q9 holds a * (Bottom Q9) = Bottom Q9 let a be Element of Q9; ::_thesis: a * (Bottom Q9) = Bottom Q9 deffunc H5( Element of Q9) -> Element of the carrier of Q9 = a [*] \$1; { H5(c) where c is Element of Q9 : S1[c] } = {} from QUANTAL1:sch_2(A2); hence a * (Bottom Q9) = Bottom Q9 by A1, Def5; ::_thesis: verum end; hence Q is BlikleNet ; ::_thesis: verum end; theorem Th8: :: QUANTAL1:8 for Q being Quantale for a, b, c being Element of Q st a [= b holds ( a [*] c [= b [*] c & c [*] a [= c [*] b ) proof let Q be Quantale; ::_thesis: for a, b, c being Element of Q st a [= b holds ( a [*] c [= b [*] c & c [*] a [= c [*] b ) let a, b, c be Element of Q; ::_thesis: ( a [= b implies ( a [*] c [= b [*] c & c [*] a [= c [*] b ) ) assume A1: a [= b ; ::_thesis: ( a [*] c [= b [*] c & c [*] a [= c [*] b ) thus (a [*] c) "\/" (b [*] c) = (a "\/" b) [*] c by Th6 .= b [*] c by A1, LATTICES:def_3 ; :: according to LATTICES:def_3 ::_thesis: c [*] a [= c [*] b thus (c [*] a) "\/" (c [*] b) = c [*] (a "\/" b) by Th6 .= c [*] b by A1, LATTICES:def_3 ; :: according to LATTICES:def_3 ::_thesis: verum end; theorem Th9: :: QUANTAL1:9 for Q being Quantale for a, b, c, d being Element of Q st a [= b & c [= d holds a [*] c [= b [*] d proof let Q be Quantale; ::_thesis: for a, b, c, d being Element of Q st a [= b & c [= d holds a [*] c [= b [*] d let a, b, c, d be Element of Q; ::_thesis: ( a [= b & c [= d implies a [*] c [= b [*] d ) assume ( a [= b & c [= d ) ; ::_thesis: a [*] c [= b [*] d then ( a [*] c [= b [*] c & b [*] c [= b [*] d ) by Th8; hence a [*] c [= b [*] d by LATTICES:7; ::_thesis: verum end; definition let f be Function; attrf is idempotent means :: QUANTAL1:def 9 f * f = f; end; :: deftheorem defines idempotent QUANTAL1:def_9_:_ for f being Function holds ( f is idempotent iff f * f = f ); Lm1: for A being non empty set for f being UnOp of A st f is idempotent holds for a being Element of A holds f . (f . a) = f . a proof let A be non empty set ; ::_thesis: for f being UnOp of A st f is idempotent holds for a being Element of A holds f . (f . a) = f . a let f be UnOp of A; ::_thesis: ( f is idempotent implies for a being Element of A holds f . (f . a) = f . a ) assume f * f = f ; :: according to QUANTAL1:def_9 ::_thesis: for a being Element of A holds f . (f . a) = f . a hence for a being Element of A holds f . (f . a) = f . a by FUNCT_2:15; ::_thesis: verum end; definition let L be non empty LattStr ; let IT be UnOp of L; attrIT is inflationary means :: QUANTAL1:def 10 for p being Element of L holds p [= IT . p; attrIT is deflationary means :: QUANTAL1:def 11 for p being Element of L holds IT . p [= p; attrIT is monotone means :Def12: :: QUANTAL1:def 12 for p, q being Element of L st p [= q holds IT . p [= IT . q; attrIT is \/-distributive means :: QUANTAL1:def 13 for X being Subset of L holds IT . ("\/" X) [= "\/" ( { (IT . a) where a is Element of L : a in X } ,L); end; :: deftheorem defines inflationary QUANTAL1:def_10_:_ for L being non empty LattStr for IT being UnOp of L holds ( IT is inflationary iff for p being Element of L holds p [= IT . p ); :: deftheorem defines deflationary QUANTAL1:def_11_:_ for L being non empty LattStr for IT being UnOp of L holds ( IT is deflationary iff for p being Element of L holds IT . p [= p ); :: deftheorem Def12 defines monotone QUANTAL1:def_12_:_ for L being non empty LattStr for IT being UnOp of L holds ( IT is monotone iff for p, q being Element of L st p [= q holds IT . p [= IT . q ); :: deftheorem defines \/-distributive QUANTAL1:def_13_:_ for L being non empty LattStr for IT being UnOp of L holds ( IT is \/-distributive iff for X being Subset of L holds IT . ("\/" X) [= "\/" ( { (IT . a) where a is Element of L : a in X } ,L) ); registration let L be Lattice; cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V17( the carrier of L) V21( the carrier of L, the carrier of L) inflationary deflationary monotone for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being UnOp of L st ( b1 is inflationary & b1 is deflationary & b1 is monotone ) proof reconsider f = id the carrier of L as UnOp of L ; take f ; ::_thesis: ( f is inflationary & f is deflationary & f is monotone ) thus f is inflationary ::_thesis: ( f is deflationary & f is monotone ) proof let p be Element of L; :: according to QUANTAL1:def_10 ::_thesis: p [= f . p p [= p ; hence p [= f . p by FUNCT_1:17; ::_thesis: verum end; thus f is deflationary ::_thesis: f is monotone proof let p be Element of L; :: according to QUANTAL1:def_11 ::_thesis: f . p [= p p [= p ; hence f . p [= p by FUNCT_1:17; ::_thesis: verum end; let p, q be Element of L; :: according to QUANTAL1:def_12 ::_thesis: ( p [= q implies f . p [= f . q ) f . p = p by FUNCT_1:17; hence ( p [= q implies f . p [= f . q ) by FUNCT_1:17; ::_thesis: verum end; end; theorem Th10: :: QUANTAL1:10 for L being complete Lattice for j being UnOp of L st j is monotone holds ( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ) proof let L be complete Lattice; ::_thesis: for j being UnOp of L st j is monotone holds ( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ) let j be UnOp of L; ::_thesis: ( j is monotone implies ( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ) ) assume A1: j is monotone ; ::_thesis: ( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ) thus ( j is \/-distributive implies for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ) ::_thesis: ( ( for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ) implies j is \/-distributive ) proof assume A2: for X being Subset of L holds j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L) ; :: according to QUANTAL1:def_13 ::_thesis: for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) let X be Subset of L; ::_thesis: j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) { (j . a) where a is Element of L : a in X } is_less_than j . ("\/" X) proof let x be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not x in { (j . a) where a is Element of L : a in X } or x [= j . ("\/" X) ) assume x in { (j . a) where a is Element of L : a in X } ; ::_thesis: x [= j . ("\/" X) then consider a being Element of L such that A3: x = j . a and A4: a in X ; a [= "\/" X by A4, LATTICE3:38; hence x [= j . ("\/" X) by A1, A3, Def12; ::_thesis: verum end; then A5: "\/" ( { (j . a) where a is Element of L : a in X } ,L) [= j . ("\/" X) by LATTICE3:def_21; j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A2; hence j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A5, LATTICES:8; ::_thesis: verum end; assume A6: for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ; ::_thesis: j is \/-distributive let X be Subset of L; :: according to QUANTAL1:def_13 ::_thesis: j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L) j . ("\/" X) [= j . ("\/" X) ; hence j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A6; ::_thesis: verum end; definition let Q be non empty QuantaleStr ; let IT be UnOp of Q; attrIT is times-monotone means :: QUANTAL1:def 14 for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b); end; :: deftheorem defines times-monotone QUANTAL1:def_14_:_ for Q being non empty QuantaleStr for IT being UnOp of Q holds ( IT is times-monotone iff for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b) ); definition let Q be non empty QuantaleStr ; let a, b be Element of Q; funca -r> b -> Element of Q equals :: QUANTAL1:def 15 "\/" ( { c where c is Element of Q : c [*] a [= b } ,Q); correctness coherence "\/" ( { c where c is Element of Q : c [*] a [= b } ,Q) is Element of Q; ; funca -l> b -> Element of Q equals :: QUANTAL1:def 16 "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q); correctness coherence "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q) is Element of Q; ; end; :: deftheorem defines -r> QUANTAL1:def_15_:_ for Q being non empty QuantaleStr for a, b being Element of Q holds a -r> b = "\/" ( { c where c is Element of Q : c [*] a [= b } ,Q); :: deftheorem defines -l> QUANTAL1:def_16_:_ for Q being non empty QuantaleStr for a, b being Element of Q holds a -l> b = "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q); theorem Th11: :: QUANTAL1:11 for Q being Quantale for a, b, c being Element of Q holds ( a [*] b [= c iff b [= a -l> c ) proof let Q be Quantale; ::_thesis: for a, b, c being Element of Q holds ( a [*] b [= c iff b [= a -l> c ) let a, b, c be Element of Q; ::_thesis: ( a [*] b [= c iff b [= a -l> c ) set X = { d where d is Element of Q : a [*] d [= c } ; { d where d is Element of Q : a [*] d [= c } c= H1(Q) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of Q : a [*] d [= c } or x in H1(Q) ) assume x in { d where d is Element of Q : a [*] d [= c } ; ::_thesis: x in H1(Q) then ex d being Element of Q st ( x = d & a [*] d [= c ) ; hence x in H1(Q) ; ::_thesis: verum end; then reconsider X = { d where d is Element of Q : a [*] d [= c } as Subset of Q ; thus ( a [*] b [= c implies b [= a -l> c ) ::_thesis: ( b [= a -l> c implies a [*] b [= c ) proof assume a [*] b [= c ; ::_thesis: b [= a -l> c then b in X ; hence b [= a -l> c by LATTICE3:38; ::_thesis: verum end; deffunc H5( Element of Q) -> Element of the carrier of Q = a [*] \$1; defpred S1[ set ] means \$1 in X; defpred S2[ Element of Q] means a [*] \$1 [= c; assume b [= a -l> c ; ::_thesis: a [*] b [= c then A1: a [*] b [= a [*] ("\/" X) by Th8; now__::_thesis:_for_d_being_Element_of_Q_st_d_in_X_holds_ a_[*]_d_[=_c let d be Element of Q; ::_thesis: ( d in X implies a [*] d [= c ) assume d in X ; ::_thesis: a [*] d [= c then ex d1 being Element of Q st ( d = d1 & a [*] d1 [= c ) ; hence a [*] d [= c ; ::_thesis: verum end; then A2: for d being Element of Q holds ( S1[d] iff S2[d] ) ; A3: { H5(d1) where d1 is Element of Q : S1[d1] } = { H5(d2) where d2 is Element of Q : S2[d2] } from FRAENKEL:sch_3(A2); A4: { (a [*] d) where d is Element of Q : d in X } is_less_than c proof let d1 be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not d1 in { (a [*] d) where d is Element of Q : d in X } or d1 [= c ) assume d1 in { (a [*] d) where d is Element of Q : d in X } ; ::_thesis: d1 [= c then ex d2 being Element of Q st ( d1 = a [*] d2 & a [*] d2 [= c ) by A3; hence d1 [= c ; ::_thesis: verum end; a [*] ("\/" X) = "\/" ( { (a [*] d) where d is Element of Q : d in X } ,Q) by Def5; then a [*] ("\/" X) [= c by A4, LATTICE3:def_21; hence a [*] b [= c by A1, LATTICES:7; ::_thesis: verum end; theorem Th12: :: QUANTAL1:12 for Q being Quantale for a, b, c being Element of Q holds ( a [*] b [= c iff a [= b -r> c ) proof let Q be Quantale; ::_thesis: for a, b, c being Element of Q holds ( a [*] b [= c iff a [= b -r> c ) let a, b, c be Element of Q; ::_thesis: ( a [*] b [= c iff a [= b -r> c ) set X = { d where d is Element of Q : d [*] b [= c } ; { d where d is Element of Q : d [*] b [= c } c= H1(Q) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of Q : d [*] b [= c } or x in H1(Q) ) assume x in { d where d is Element of Q : d [*] b [= c } ; ::_thesis: x in H1(Q) then ex d being Element of Q st ( x = d & d [*] b [= c ) ; hence x in H1(Q) ; ::_thesis: verum end; then reconsider X = { d where d is Element of Q : d [*] b [= c } as Subset of Q ; thus ( a [*] b [= c implies a [= b -r> c ) ::_thesis: ( a [= b -r> c implies a [*] b [= c ) proof assume a [*] b [= c ; ::_thesis: a [= b -r> c then a in X ; hence a [= b -r> c by LATTICE3:38; ::_thesis: verum end; deffunc H5( Element of Q) -> Element of the carrier of Q = \$1 [*] b; defpred S1[ set ] means \$1 in X; defpred S2[ Element of Q] means \$1 [*] b [= c; assume a [= b -r> c ; ::_thesis: a [*] b [= c then A1: a [*] b [= ("\/" X) [*] b by Th8; now__::_thesis:_for_d_being_Element_of_Q_st_d_in_X_holds_ d_[*]_b_[=_c let d be Element of Q; ::_thesis: ( d in X implies d [*] b [= c ) assume d in X ; ::_thesis: d [*] b [= c then ex d1 being Element of Q st ( d = d1 & d1 [*] b [= c ) ; hence d [*] b [= c ; ::_thesis: verum end; then A2: for d being Element of Q holds ( S1[d] iff S2[d] ) ; A3: { H5(d1) where d1 is Element of Q : S1[d1] } = { H5(d2) where d2 is Element of Q : S2[d2] } from FRAENKEL:sch_3(A2); A4: { (d [*] b) where d is Element of Q : d in X } is_less_than c proof let d1 be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not d1 in { (d [*] b) where d is Element of Q : d in X } or d1 [= c ) assume d1 in { (d [*] b) where d is Element of Q : d in X } ; ::_thesis: d1 [= c then ex d2 being Element of Q st ( d1 = d2 [*] b & d2 [*] b [= c ) by A3; hence d1 [= c ; ::_thesis: verum end; ("\/" X) [*] b = "\/" ( { (d [*] b) where d is Element of Q : d in X } ,Q) by Def6; then ("\/" X) [*] b [= c by A4, LATTICE3:def_21; hence a [*] b [= c by A1, LATTICES:7; ::_thesis: verum end; theorem Th13: :: QUANTAL1:13 for Q being Quantale for s, a, b being Element of Q st a [= b holds ( b -r> s [= a -r> s & b -l> s [= a -l> s ) proof let Q be Quantale; ::_thesis: for s, a, b being Element of Q st a [= b holds ( b -r> s [= a -r> s & b -l> s [= a -l> s ) let s, a, b be Element of Q; ::_thesis: ( a [= b implies ( b -r> s [= a -r> s & b -l> s [= a -l> s ) ) assume A1: a [= b ; ::_thesis: ( b -r> s [= a -r> s & b -l> s [= a -l> s ) { d where d is Element of Q : d [*] b [= s } c= { c where c is Element of Q : c [*] a [= s } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of Q : d [*] b [= s } or x in { c where c is Element of Q : c [*] a [= s } ) assume x in { d where d is Element of Q : d [*] b [= s } ; ::_thesis: x in { c where c is Element of Q : c [*] a [= s } then consider d being 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 x in { c where c is Element of Q : c [*] a [= s } by A2; ::_thesis: verum end; hence b -r> s [= a -r> s by LATTICE3:45; ::_thesis: b -l> s [= a -l> s { d where d is Element of Q : b [*] d [= s } c= { c where c is Element of Q : a [*] c [= s } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of Q : b [*] d [= s } or x in { c where c is Element of Q : a [*] c [= s } ) assume x in { d where d is Element of Q : b [*] d [= s } ; ::_thesis: x in { c where c is Element of Q : a [*] c [= s } then consider d being 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 x in { c where c is Element of Q : a [*] c [= s } by A4; ::_thesis: verum end; hence b -l> s [= a -l> s by LATTICE3:45; ::_thesis: verum end; theorem :: QUANTAL1:14 for Q being Quantale for s being Element of Q for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds j is monotone proof let Q be Quantale; ::_thesis: for s being Element of Q for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds j is monotone let s be Element of Q; ::_thesis: for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds j is monotone let j be UnOp of Q; ::_thesis: ( ( for a being Element of Q holds j . a = (a -r> s) -r> s ) implies j is monotone ) assume A1: for a being Element of Q holds j . a = (a -r> s) -r> s ; ::_thesis: j is monotone thus j is monotone ::_thesis: verum proof let a, b be Element of Q; :: according to QUANTAL1:def_12 ::_thesis: ( a [= b implies j . a [= j . b ) assume a [= b ; ::_thesis: j . a [= j . 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 j . a [= j . b by A1, A2; ::_thesis: verum end; end; definition let Q be non empty QuantaleStr ; let IT be Element of Q; attrIT is dualizing means :Def17: :: QUANTAL1:def 17 for a being Element of Q holds ( (a -r> IT) -l> IT = a & (a -l> IT) -r> IT = a ); attrIT is cyclic means :Def18: :: QUANTAL1:def 18 for a being Element of Q holds a -r> IT = a -l> IT; end; :: deftheorem Def17 defines dualizing QUANTAL1:def_17_:_ for Q being non empty QuantaleStr for IT being Element of Q holds ( IT is dualizing iff for a being Element of Q holds ( (a -r> IT) -l> IT = a & (a -l> IT) -r> IT = a ) ); :: deftheorem Def18 defines cyclic QUANTAL1:def_18_:_ for Q being non empty QuantaleStr for IT being Element of Q holds ( IT is cyclic iff for a being Element of Q holds a -r> IT = a -l> IT ); theorem Th15: :: QUANTAL1:15 for Q being Quantale for c being Element of Q holds ( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds b [*] a [= c ) proof let Q be Quantale; ::_thesis: for c being Element of Q holds ( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds b [*] a [= c ) let c be Element of Q; ::_thesis: ( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds b [*] a [= c ) thus ( c is cyclic implies for a, b being Element of Q st a [*] b [= c holds b [*] a [= c ) ::_thesis: ( ( for a, b being Element of Q st a [*] b [= c holds b [*] a [= c ) implies c is cyclic ) proof assume A1: for a being Element of Q holds a -r> c = a -l> c ; :: according to QUANTAL1:def_18 ::_thesis: for a, b being Element of Q st a [*] b [= c holds b [*] a [= c let a, b be Element of Q; ::_thesis: ( a [*] b [= c implies b [*] a [= c ) assume a [*] b [= c ; ::_thesis: b [*] a [= c then a [= b -r> c by Th12; then a [= b -l> c by A1; hence b [*] a [= c by Th11; ::_thesis: verum end; assume A2: for a, b being Element of Q st a [*] b [= c holds b [*] a [= c ; ::_thesis: c is cyclic let a be Element of Q; :: according to QUANTAL1:def_18 ::_thesis: a -r> c = a -l> c set X1 = { d1 where d1 is Element of Q : d1 [*] a [= c } ; set X2 = { d2 where d2 is Element of Q : a [*] d2 [= c } ; { d1 where d1 is Element of Q : d1 [*] a [= c } = { d2 where d2 is Element of Q : a [*] d2 [= c } proof thus { d1 where d1 is Element of Q : d1 [*] a [= c } c= { d2 where d2 is Element of Q : a [*] d2 [= c } :: according to XBOOLE_0:def_10 ::_thesis: { d2 where d2 is Element of Q : a [*] d2 [= c } c= { d1 where d1 is Element of Q : d1 [*] a [= c } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d1 where d1 is Element of Q : d1 [*] a [= c } or x in { d2 where d2 is Element of Q : a [*] d2 [= c } ) assume x in { d1 where d1 is Element of Q : d1 [*] a [= c } ; ::_thesis: x in { d2 where d2 is Element of Q : a [*] d2 [= c } then consider d being Element of Q such that A3: x = d and A4: d [*] a [= c ; a [*] d [= c by A2, A4; hence x in { d2 where d2 is Element of Q : a [*] d2 [= c } by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d2 where d2 is Element of Q : a [*] d2 [= c } or x in { d1 where d1 is Element of Q : d1 [*] a [= c } ) assume x in { d2 where d2 is Element of Q : a [*] d2 [= c } ; ::_thesis: x in { d1 where d1 is Element of Q : d1 [*] a [= c } then consider d being Element of Q such that A5: x = d and A6: a [*] d [= c ; d [*] a [= c by A2, A6; hence x in { d1 where d1 is Element of Q : d1 [*] a [= c } by A5; ::_thesis: verum end; hence a -r> c = a -l> c ; ::_thesis: verum end; theorem Th16: :: QUANTAL1:16 for Q being Quantale for s, a being Element of Q st s is cyclic holds ( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s ) proof let Q be Quantale; ::_thesis: for s, a being Element of Q st s is cyclic holds ( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s ) let s, a be Element of Q; ::_thesis: ( s is cyclic implies ( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s ) ) assume A1: s is cyclic ; ::_thesis: ( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s ) A2: { b where b is Element of Q : b [= a } c= { c where c is Element of Q : c [*] (a -r> s) [= s } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { b where b is Element of Q : b [= a } or x in { c where c is Element of Q : c [*] (a -r> s) [= s } ) assume x in { b where b is Element of Q : b [= a } ; ::_thesis: x in { c where c is Element of Q : c [*] (a -r> s) [= s } then consider b being Element of Q 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 x in { c where c is Element of Q : c [*] (a -r> s) [= s } by A3; ::_thesis: verum end; A6: { b where b is Element of Q : b [= a } c= { c where c is Element of Q : (a -l> s) [*] c [= s } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { b where b is Element of Q : b [= a } or x in { c where c is Element of Q : (a -l> s) [*] c [= s } ) assume x in { b where b is Element of Q : b [= a } ; ::_thesis: x in { c where c is Element of Q : (a -l> s) [*] c [= s } then consider b being Element of Q 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 x in { c where c is Element of Q : (a -l> s) [*] c [= s } by A7; ::_thesis: verum end; a = "\/" ( { d where d is Element of Q : d [= a } ,Q) by LATTICE3:44; hence a [= (a -r> s) -r> s by A2, LATTICE3:45; ::_thesis: a [= (a -l> s) -l> s a = "\/" ( { d where d is Element of Q : d [= a } ,Q) by LATTICE3:44; hence a [= (a -l> s) -l> s by A6, LATTICE3:45; ::_thesis: verum end; theorem :: QUANTAL1:17 for Q being Quantale for s, a being 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 be Quantale; ::_thesis: for s, a being 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 ) let s, a be Element of Q; ::_thesis: ( s is cyclic implies ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s ) ) assume A1: s is cyclic ; ::_thesis: ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s ) 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 ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s ) by A2, A3, LATTICES:8; ::_thesis: verum end; theorem :: QUANTAL1:18 for Q being Quantale for s, a, b being Element of Q holds ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s proof let Q be Quantale; ::_thesis: for s, a, b being Element of Q holds ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s let s, a, b be Element of Q; ::_thesis: ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s deffunc H5( Element of Q) -> set = { c where c is Element of Q : c [*] (\$1 -r> s) [= s } ; A1: { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H5(a) & b9 in H5(b) ) } c= H5(a [*] b) proof defpred S1[ Element of Q] means \$1 [*] (a [*] b) [= s; deffunc H6( Element of Q) -> Element of Q = \$1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H5(a) & b9 in H5(b) ) } or x in H5(a [*] b) ) set A = { H6(c) where c is Element of Q : S1[c] } ; assume x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H5(a) & b9 in H5(b) ) } ; ::_thesis: x in H5(a [*] b) then consider a9, b9 being Element of Q such that A2: x = a9 [*] b9 and A3: a9 in H5(a) and A4: b9 in H5(b) ; deffunc H7( Element of Q) -> Element of the carrier of Q = (a9 [*] b9) [*] \$1; set B = { H7(H6(c)) where c is Element of Q : S1[c] } ; A5: ex c being Element of Q st ( b9 = c & c [*] (b -r> s) [= s ) by A4; A6: ex c being Element of Q st ( a9 = c & c [*] (a -r> s) [= s ) by A3; A7: { H7(H6(c)) where c is Element of Q : S1[c] } is_less_than s proof let d be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not d in { H7(H6(c)) where c is Element of Q : S1[c] } or d [= s ) assume d in { H7(H6(c)) where c is Element of Q : S1[c] } ; ::_thesis: d [= s then consider c being Element of Q 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; ::_thesis: verum end; { H7(c) where c is Element of Q : c in { H6(c) where c is Element of Q : S1[c] } } = { H7(H6(c)) where c is Element of Q : S1[c] } from QUANTAL1:sch_1(); then (a9 [*] b9) [*] ((a [*] b) -r> s) = "\/" ( { H7(H6(c)) where c is Element of Q : S1[c] } ,Q) by Def5; then (a9 [*] b9) [*] ((a [*] b) -r> s) [= s by A7, LATTICE3:def_21; hence x in H5(a [*] b) by A2; ::_thesis: verum end; ((a -r> s) -r> s) [*] ((b -r> s) -r> s) = "\/" ( { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H5(a) & b9 in H5(b) ) } ,Q) by Th5; hence ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s by A1, LATTICE3:45; ::_thesis: verum end; theorem Th19: :: QUANTAL1:19 for Q being Quantale for D being Element of Q st D is dualizing holds ( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) proof let Q be Quantale; ::_thesis: for D being Element of Q st D is dualizing holds ( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) let D be Element of Q; ::_thesis: ( 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 ) ) set I = D -l> D; set J = D -r> D; assume A1: for a being Element of Q holds ( (a -r> D) -l> D = a & (a -l> D) -r> D = a ) ; :: according to QUANTAL1:def_17 ::_thesis: ( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) A2: now__::_thesis:_for_a_being_Element_of_Q_holds_ (_a_[*]_(D_-l>_D)_=_a_&_(D_-r>_D)_[*]_a_=_a_) deffunc H5( set ) -> set = \$1; let a be Element of Q; ::_thesis: ( a [*] (D -l> D) = a & (D -r> D) [*] a = a ) defpred S1[ Element of Q] means \$1 [*] (a [*] (D -l> D)) [= D; defpred S2[ Element of Q] means \$1 [*] a [= D; defpred S3[ Element of Q] means ((D -r> D) [*] a) [*] \$1 [= D; defpred S4[ Element of Q] means a [*] \$1 [= D; A3: for b being Element of Q holds ( S1[b] iff S2[b] ) proof let b be Element of Q; ::_thesis: ( S1[b] iff S2[b] ) ( b [*] (a [*] (D -l> D)) = (b [*] a) [*] (D -l> D) & (D -l> D) -r> D = D ) by A1, GROUP_1:def_3; hence ( S1[b] iff S2[b] ) by Th12; ::_thesis: verum end; A4: { H5(b) where b is Element of Q : S1[b] } = { H5(c) where c is Element of Q : S2[c] } from FRAENKEL:sch_3(A3); thus a [*] (D -l> D) = ((a [*] (D -l> D)) -r> D) -l> D by A1 .= (a -r> D) -l> D by A4 .= a by A1 ; ::_thesis: (D -r> D) [*] a = a A5: for b being Element of Q holds ( S3[b] iff S4[b] ) proof let b be Element of Q; ::_thesis: ( S3[b] iff S4[b] ) ( (D -r> D) [*] (a [*] b) = ((D -r> D) [*] a) [*] b & (D -r> D) -l> D = D ) by A1, GROUP_1:def_3; hence ( S3[b] iff S4[b] ) by Th11; ::_thesis: verum end; A6: { H5(b) where b is Element of Q : S3[b] } = { H5(c) where c is Element of Q : S4[c] } from FRAENKEL:sch_3(A5); thus (D -r> D) [*] a = (((D -r> D) [*] a) -l> D) -r> D by A1 .= (a -l> D) -r> D by A6 .= a by A1 ; ::_thesis: verum end; A7: D -l> D is_a_right_unity_wrt H4(Q) proof let a be Element of Q; :: according to BINOP_1:def_17 ::_thesis: H4(Q) . (a,(D -l> D)) = a thus H4(Q) . (a,(D -l> D)) = a [*] (D -l> D) .= a by A2 ; ::_thesis: verum end; A8: D -l> D = (D -r> D) [*] (D -l> D) by A2; D -l> D is_a_left_unity_wrt H4(Q) proof let a be Element of Q; :: according to BINOP_1:def_16 ::_thesis: H4(Q) . ((D -l> D),a) = a thus H4(Q) . ((D -l> D),a) = (D -r> D) [*] a by A2, A8 .= a by A2 ; ::_thesis: verum end; then A9: D -l> D is_a_unity_wrt H4(Q) by A7, BINOP_1:def_7; hence H4(Q) is having_a_unity by SETWISEO:def_2; :: according to MONOID_0:def_10 ::_thesis: ( the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) D -r> D = (D -r> D) [*] (D -l> D) by A2; hence ( the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) by A8, A9, BINOP_1:def_8; ::_thesis: verum end; theorem :: QUANTAL1:20 for Q being Quantale for a, b, c being Element of Q st a is dualizing holds ( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a ) proof let Q be Quantale; ::_thesis: for a, b, c being Element of Q st a is dualizing holds ( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a ) let a, b, c be Element of Q; ::_thesis: ( a is dualizing implies ( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a ) ) deffunc H5( set ) -> set = \$1; defpred S1[ Element of Q] means \$1 [*] b [= c; defpred S2[ Element of Q] means \$1 [*] (b [*] (c -l> a)) [= a; defpred S3[ Element of Q] means b [*] \$1 [= c; defpred S4[ Element of Q] means ((c -r> a) [*] b) [*] \$1 [= a; assume A1: for d being Element of Q holds ( (d -r> a) -l> a = d & (d -l> a) -r> a = d ) ; :: according to QUANTAL1:def_17 ::_thesis: ( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a ) then A2: c = (c -l> a) -r> a ; A3: for d being Element of Q holds ( S1[d] iff S2[d] ) proof let d be Element of Q; ::_thesis: ( S1[d] iff S2[d] ) d [*] (b [*] (c -l> a)) = (d [*] b) [*] (c -l> a) by GROUP_1:def_3; hence ( S1[d] iff S2[d] ) by A2, Th12; ::_thesis: verum end; { H5(d1) where d1 is Element of Q : S1[d1] } = { H5(d2) where d2 is Element of Q : S2[d2] } from FRAENKEL:sch_3(A3); hence b -r> c = (b [*] (c -l> a)) -r> a ; ::_thesis: b -l> c = ((c -r> a) [*] b) -l> a A4: c = (c -r> a) -l> a by A1; A5: for d being Element of Q holds ( S3[d] iff S4[d] ) proof let d be Element of Q; ::_thesis: ( S3[d] iff S4[d] ) ((c -r> a) [*] b) [*] d = (c -r> a) [*] (b [*] d) by GROUP_1:def_3; hence ( S3[d] iff S4[d] ) by A4, Th11; ::_thesis: verum end; { H5(d1) where d1 is Element of Q : S3[d1] } = { H5(d2) where d2 is Element of Q : S4[d2] } from FRAENKEL:sch_3(A5); hence b -l> c = ((c -r> a) [*] b) -l> a ; ::_thesis: verum end; definition attrc1 is strict ; struct Girard-QuantaleStr -> QuasiNetStr ; aggrGirard-QuantaleStr(# carrier, L_join, L_meet, multF, OneF, absurd #) -> Girard-QuantaleStr ; sel absurd c1 -> Element of the carrier of c1; end; registration cluster non empty for Girard-QuantaleStr ; existence not for b1 being Girard-QuantaleStr holds b1 is empty proof set A = the non empty set ; set b1 = the BinOp of the non empty set ; set e1 = the Element of the non empty set ; take Girard-QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Element of the non empty set #) ; ::_thesis: not Girard-QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty thus not the carrier of Girard-QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; definition let IT be non empty Girard-QuantaleStr ; attrIT is cyclic means :Def19: :: QUANTAL1:def 19 the absurd of IT is cyclic ; attrIT is dualized means :Def20: :: QUANTAL1:def 20 the absurd of IT is dualizing ; end; :: deftheorem Def19 defines cyclic QUANTAL1:def_19_:_ for IT being non empty Girard-QuantaleStr holds ( IT is cyclic iff the absurd of IT is cyclic ); :: deftheorem Def20 defines dualized QUANTAL1:def_20_:_ for IT being non empty Girard-QuantaleStr holds ( IT is dualized iff the absurd of IT is dualizing ); theorem Th21: :: QUANTAL1:21 for Q being non empty Girard-QuantaleStr st LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} holds ( Q is cyclic & Q is dualized ) proof let Q be non empty Girard-QuantaleStr ; ::_thesis: ( LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} implies ( Q is cyclic & Q is dualized ) ) set c = the absurd of Q; assume LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} ; ::_thesis: ( Q is cyclic & Q is dualized ) then A1: H1(Q) = {{}} by LATTICE3:def_1, ZFMISC_1:1; thus Q is cyclic ::_thesis: Q is dualized proof let a be Element of Q; :: according to QUANTAL1:def_18,QUANTAL1:def_19 ::_thesis: a -r> the absurd of Q = a -l> the absurd of Q a -r> the absurd of Q = {} by A1, TARSKI:def_1; hence a -r> the absurd of Q = a -l> the absurd of Q by A1, TARSKI:def_1; ::_thesis: verum end; let a be Element of Q; :: according to QUANTAL1:def_17,QUANTAL1:def_20 ::_thesis: ( (a -r> the absurd of Q) -l> the absurd of Q = a & (a -l> the absurd of Q) -r> the absurd of Q = a ) ( (a -r> the absurd of Q) -l> the absurd of Q = {} & (a -l> the absurd of Q) -r> the absurd of Q = {} ) by A1, TARSKI:def_1; hence ( (a -r> the absurd of Q) -l> the absurd of Q = a & (a -l> the absurd of Q) -r> the absurd of Q = a ) by A1, TARSKI:def_1; ::_thesis: verum end; registration let A be non empty set ; let b1, b2, b3 be BinOp of A; let e1, e2 be Element of A; cluster Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) -> non empty ; coherence not Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) is empty ; end; registration cluster non empty unital associative commutative Lattice-like complete right-distributive left-distributive strict cyclic dualized for Girard-QuantaleStr ; existence ex b1 being non empty Girard-QuantaleStr st ( b1 is associative & b1 is commutative & b1 is unital & b1 is left-distributive & b1 is right-distributive & b1 is complete & b1 is Lattice-like & b1 is cyclic & b1 is dualized & b1 is strict ) proof set B = BooleLatt {}; set b = the BinOp of (BooleLatt {}); set e = the Element of (BooleLatt {}); take Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) ; ::_thesis: ( Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is associative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is commutative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is unital & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is left-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is right-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is complete & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is Lattice-like & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is cyclic & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is dualized & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is strict ) thus ( Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is associative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is commutative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is unital & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is left-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is right-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is complete & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is Lattice-like & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is cyclic & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is dualized & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is strict ) by Th4, Th21; ::_thesis: verum end; end; definition mode Girard-Quantale is non empty unital associative Lattice-like complete right-distributive left-distributive cyclic dualized Girard-QuantaleStr ; end; definition let G be Girard-QuantaleStr ; func Bottom G -> Element of G equals :: QUANTAL1:def 21 the absurd of G; correctness coherence the absurd of G is Element of G; ; end; :: deftheorem defines Bottom QUANTAL1:def_21_:_ for G being Girard-QuantaleStr holds Bottom G = the absurd of G; definition let G be non empty Girard-QuantaleStr ; func Top G -> Element of G equals :: QUANTAL1:def 22 (Bottom G) -r> (Bottom G); correctness coherence (Bottom G) -r> (Bottom G) is Element of G; ; let a be Element of G; func Bottom a -> Element of G equals :: QUANTAL1:def 23 a -r> (Bottom G); correctness coherence a -r> (Bottom G) is Element of G; ; end; :: deftheorem defines Top QUANTAL1:def_22_:_ for G being non empty Girard-QuantaleStr holds Top G = (Bottom G) -r> (Bottom G); :: deftheorem defines Bottom QUANTAL1:def_23_:_ for G being non empty Girard-QuantaleStr for a being Element of G holds Bottom a = a -r> (Bottom G); definition let G be non empty Girard-QuantaleStr ; func Negation G -> UnOp of G means :: QUANTAL1:def 24 for a being Element of G holds it . a = Bottom a; existence ex b1 being UnOp of G st for a being Element of G holds b1 . a = Bottom a proof deffunc H5( Element of G) -> Element of G = Bottom \$1; consider f being Function of the carrier of G, the carrier of G such that A1: for a being Element of G holds f . a = H5(a) from FUNCT_2:sch_4(); reconsider f = f as UnOp of G ; take f ; ::_thesis: for a being Element of G holds f . a = Bottom a thus for a being Element of G holds f . a = Bottom a by A1; ::_thesis: verum end; uniqueness for b1, b2 being UnOp of G st ( for a being Element of G holds b1 . a = Bottom a ) & ( for a being Element of G holds b2 . a = Bottom a ) holds b1 = b2 proof let f1, f2 be UnOp of G; ::_thesis: ( ( for a being Element of G holds f1 . a = Bottom a ) & ( for a being Element of G holds f2 . a = Bottom a ) implies f1 = f2 ) assume that A2: for a being Element of G holds f1 . a = Bottom a and A3: for a being Element of G holds f2 . a = Bottom a ; ::_thesis: f1 = f2 now__::_thesis:_for_a_being_Element_of_G_holds_f1_._a_=_f2_._a let a be Element of G; ::_thesis: f1 . a = f2 . a thus f1 . a = Bottom a by A2 .= f2 . a by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines Negation QUANTAL1:def_24_:_ for G being non empty Girard-QuantaleStr for b2 being UnOp of G holds ( b2 = Negation G iff for a being Element of G holds b2 . a = Bottom a ); definition let G be non empty Girard-QuantaleStr ; let u be UnOp of G; func Bottom u -> UnOp of G equals :: QUANTAL1:def 25 (Negation G) * u; correctness coherence (Negation G) * u is UnOp of G; ; end; :: deftheorem defines Bottom QUANTAL1:def_25_:_ for G being non empty Girard-QuantaleStr for u being UnOp of G holds Bottom u = (Negation G) * u; definition let G be non empty Girard-QuantaleStr ; let o be BinOp of G; func Bottom o -> BinOp of G equals :: QUANTAL1:def 26 (Negation G) * o; correctness coherence (Negation G) * o is BinOp of G; ; end; :: deftheorem defines Bottom QUANTAL1:def_26_:_ for G being non empty Girard-QuantaleStr for o being BinOp of G holds Bottom o = (Negation G) * o; theorem Th22: :: QUANTAL1:22 for Q being Girard-Quantale for a being Element of Q holds Bottom (Bottom a) = a proof let Q be Girard-Quantale; ::_thesis: for a being Element of Q holds Bottom (Bottom a) = a let a be Element of Q; ::_thesis: Bottom (Bottom a) = a the absurd of Q is cyclic by Def19; then A1: a -l> the absurd of Q = a -r> the absurd of Q by Def18; the absurd of Q is dualizing by Def20; hence Bottom (Bottom a) = a by A1, Def17; ::_thesis: verum end; theorem :: QUANTAL1:23 for Q being Girard-Quantale for a, b being Element of Q st a [= b holds Bottom b [= Bottom a by Th13; theorem Th24: :: QUANTAL1:24 for Q being Girard-Quantale for X being set holds Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) proof let Q be Girard-Quantale; ::_thesis: for X being set holds Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) let X be set ; ::_thesis: Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } is_less_than Bottom Q proof let c be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not c in { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } or c [= Bottom Q ) assume c in { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } ; ::_thesis: c [= Bottom Q then consider b being Element of Q such that A1: ( c = ("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b & b in X ) ; Bottom b in { (Bottom a) where a is Element of Q : a in X } by A1; then "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) [= Bottom b by LATTICE3:38; hence c [= Bottom Q by A1, Th12; ::_thesis: verum end; then "\/" ( { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } ,Q) [= Bottom Q by LATTICE3:def_21; then ("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] ("\/" (X,Q)) [= Bottom Q by Def5; then A2: "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) [= Bottom ("\/" (X,Q)) by Th12; Bottom ("\/" (X,Q)) is_less_than { (Bottom a) where a is Element of Q : a in X } proof let b be Element of Q; :: according to LATTICE3:def_16 ::_thesis: ( not b in { (Bottom a) where a is Element of Q : a in X } or Bottom ("\/" (X,Q)) [= b ) assume b in { (Bottom a) where a is Element of Q : a in X } ; ::_thesis: Bottom ("\/" (X,Q)) [= b then consider a being Element of Q such that A3: b = Bottom a and A4: a in X ; a [= "\/" (X,Q) by A4, LATTICE3:38; hence Bottom ("\/" (X,Q)) [= b by A3, Th13; ::_thesis: verum end; then Bottom ("\/" (X,Q)) [= "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by LATTICE3:39; hence Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by A2, LATTICES:8; ::_thesis: verum end; theorem Th25: :: QUANTAL1:25 for Q being Girard-Quantale for X being set holds Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q) proof let Q be Girard-Quantale; ::_thesis: for X being set holds Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q) let X be set ; ::_thesis: Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q) X is_greater_than "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) proof let c be Element of Q; :: according to LATTICE3:def_16 ::_thesis: ( not c in X or "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c ) assume c in X ; ::_thesis: "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c then Bottom c in { (Bottom b) where b is Element of Q : b in X } ; then A1: Bottom (Bottom c) in { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ; Bottom (Bottom c) = c by Th22; hence "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c by A1, LATTICE3:38; ::_thesis: verum end; then A2: "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= "/\" (X,Q) by LATTICE3:39; { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } or x in X ) assume x in { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ; ::_thesis: x in X then consider a being Element of Q such that A3: ( x = Bottom a & a in { (Bottom b) where b is Element of Q : b in X } ) ; ex b being Element of Q st ( a = Bottom b & b in X ) by A3; hence x in X by A3, Th22; ::_thesis: verum end; then "/\" (X,Q) [= "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) by LATTICE3:45; then "/\" (X,Q) = "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) by A2, LATTICES:8; hence Bottom ("/\" (X,Q)) = Bottom (Bottom ("\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q))) by Th24 .= "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by Th22 ; ::_thesis: verum end; theorem Th26: :: QUANTAL1:26 for Q being Girard-Quantale for a, b being Element of Q holds ( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) ) proof let Q be Girard-Quantale; ::_thesis: for a, b being Element of Q holds ( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) ) let a, b be Element of Q; ::_thesis: ( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) ) A1: { (Bottom c) where c is Element of Q : c in {a,b} } = {(Bottom a),(Bottom b)} proof thus { (Bottom c) where c is Element of Q : c in {a,b} } c= {(Bottom a),(Bottom b)} :: according to XBOOLE_0:def_10 ::_thesis: {(Bottom a),(Bottom b)} c= { (Bottom c) where c is Element of Q : c in {a,b} } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Bottom c) where c is Element of Q : c in {a,b} } or x in {(Bottom a),(Bottom b)} ) assume x in { (Bottom c) where c is Element of Q : c in {a,b} } ; ::_thesis: x in {(Bottom a),(Bottom b)} then consider c being Element of Q such that A2: x = Bottom c and A3: c in {a,b} ; ( c = a or c = b ) by A3, TARSKI:def_2; hence x in {(Bottom a),(Bottom b)} by A2, TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Bottom a),(Bottom b)} or x in { (Bottom c) where c is Element of Q : c in {a,b} } ) assume x in {(Bottom a),(Bottom b)} ; ::_thesis: x in { (Bottom c) where c is Element of Q : c in {a,b} } then ( ( x = Bottom a & a in {a,b} ) or ( x = Bottom b & b in {a,b} ) ) by TARSKI:def_2; hence x in { (Bottom c) where c is Element of Q : c in {a,b} } ; ::_thesis: verum 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; ::_thesis: Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) ( (Bottom a) "\/" (Bottom b) = "\/" {(Bottom a),(Bottom b)} & a "/\" b = "/\" {a,b} ) by LATTICE3:43; hence Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) by A1, Th25; ::_thesis: verum end; definition let Q be Girard-Quantale; let a, b be Element of Q; funca delta b -> Element of Q equals :: QUANTAL1:def 27 Bottom ((Bottom a) [*] (Bottom b)); correctness coherence Bottom ((Bottom a) [*] (Bottom b)) is Element of Q; ; end; :: deftheorem defines delta QUANTAL1:def_27_:_ for Q being Girard-Quantale for a, b being Element of Q holds a delta b = Bottom ((Bottom a) [*] (Bottom b)); theorem :: QUANTAL1:27 for Q being Girard-Quantale for a being Element of Q for X being set holds ( a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) & a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q) ) proof let Q be Girard-Quantale; ::_thesis: for a being Element of Q for X being set holds ( a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) & a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q) ) let a be Element of Q; ::_thesis: for X being set holds ( a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) & a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q) ) let X be set ; ::_thesis: ( a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) & a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q) ) deffunc H5( Element of Q) -> Element of the carrier of Q = (Bottom a) [*] \$1; deffunc H6( Element of Q) -> Element of Q = Bottom \$1; deffunc H7( Element of Q) -> Element of the carrier of Q = (Bottom a) [*] (Bottom \$1); defpred S1[ set ] means \$1 in X; deffunc H8( Element of Q) -> Element of Q = Bottom ((Bottom a) [*] (Bottom \$1)); deffunc H9( Element of Q) -> Element of Q = a delta \$1; thus a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) by Def5; ::_thesis: a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q) A1: { H5(c) where c is Element of Q : c in { H6(d) where d is Element of Q : S1[d] } } = { H5(H6(b)) where b is Element of Q : S1[b] } from QUANTAL1:sch_1(); A2: { H6(c) where c is Element of Q : c in { H7(d) where d is Element of Q : S1[d] } } = { H6(H7(b)) where b is Element of Q : S1[b] } from QUANTAL1:sch_1(); A3: for b being Element of Q holds H8(b) = H9(b) ; A4: { H8(b) where b is Element of Q : S1[b] } = { H9(c) where c is Element of Q : S1[c] } from FRAENKEL:sch_5(A3); thus a delta ("/\" (X,Q)) = Bottom ((Bottom a) [*] ("\/" ( { (Bottom b) where b is Element of Q : b in X } ,Q))) by Th25 .= Bottom ("\/" ( { ((Bottom a) [*] (Bottom b)) where b is Element of Q : b in X } ,Q)) by A1, Def5 .= "/\" ( { (a delta b) where b is Element of Q : b in X } ,Q) by A2, A4, Th24 ; ::_thesis: verum end; theorem :: QUANTAL1:28 for Q being Girard-Quantale for a being Element of Q for X being set holds ( ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) & ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) ) proof let Q be Girard-Quantale; ::_thesis: for a being Element of Q for X being set holds ( ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) & ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) ) let a be Element of Q; ::_thesis: for X being set holds ( ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) & ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) ) let X be set ; ::_thesis: ( ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) & ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) ) deffunc H5( Element of Q) -> Element of the carrier of Q = \$1 [*] (Bottom a); deffunc H6( Element of Q) -> Element of Q = Bottom \$1; deffunc H7( Element of Q) -> Element of the carrier of Q = (Bottom \$1) [*] (Bottom a); defpred S1[ set ] means \$1 in X; deffunc H8( Element of Q) -> Element of Q = Bottom ((Bottom \$1) [*] (Bottom a)); deffunc H9( Element of Q) -> Element of Q = \$1 delta a; thus ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) by Def6; ::_thesis: ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) A1: { H5(c) where c is Element of Q : c in { H6(d) where d is Element of Q : S1[d] } } = { H5(H6(b)) where b is Element of Q : S1[b] } from QUANTAL1:sch_1(); A2: { H6(c) where c is Element of Q : c in { H7(d) where d is Element of Q : S1[d] } } = { H6(H7(b)) where b is Element of Q : S1[b] } from QUANTAL1:sch_1(); A3: for b being Element of Q holds H8(b) = H9(b) ; A4: { H8(b) where b is Element of Q : S1[b] } = { H9(c) where c is Element of Q : S1[c] } from FRAENKEL:sch_5(A3); thus ("/\" (X,Q)) delta a = Bottom (("\/" ( { (Bottom b) where b is Element of Q : b in X } ,Q)) [*] (Bottom a)) by Th25 .= Bottom ("\/" ( { ((Bottom b) [*] (Bottom a)) where b is Element of Q : b in X } ,Q)) by A1, Def6 .= "/\" ( { (b delta a) where b is Element of Q : b in X } ,Q) by A2, A4, Th24 ; ::_thesis: verum end; theorem :: QUANTAL1:29 for Q being Girard-Quantale for a, b, c being Element of Q holds ( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) ) proof let Q be Girard-Quantale; ::_thesis: for a, b, c being Element of Q holds ( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) ) let a, b, c be Element of Q; ::_thesis: ( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) ) 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 ; ::_thesis: (b "/\" c) delta a = (b delta a) "/\" (c delta a) 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 ; ::_thesis: verum end; theorem :: QUANTAL1:30 for Q being Girard-Quantale for a1, b1, a2, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds a1 delta a2 [= b1 delta b2 proof let Q be Girard-Quantale; ::_thesis: for a1, b1, a2, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds a1 delta a2 [= b1 delta b2 let a1, b1, a2, b2 be Element of Q; ::_thesis: ( a1 [= b1 & a2 [= b2 implies a1 delta a2 [= b1 delta b2 ) assume ( a1 [= b1 & a2 [= b2 ) ; ::_thesis: a1 delta a2 [= b1 delta b2 then ( Bottom b1 [= Bottom a1 & Bottom b2 [= Bottom a2 ) by Th13; then (Bottom b1) [*] (Bottom b2) [= (Bottom a1) [*] (Bottom a2) by Th9; hence a1 delta a2 [= b1 delta b2 by Th13; ::_thesis: verum end; theorem :: QUANTAL1:31 for Q being Girard-Quantale for a, b, c being Element of Q holds (a delta b) delta c = a delta (b delta c) proof let Q be Girard-Quantale; ::_thesis: for a, b, c being Element of Q holds (a delta b) delta c = a delta (b delta c) let a, b, c be Element of Q; ::_thesis: (a delta b) delta c = a delta (b delta c) 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 ; ::_thesis: verum end; theorem Th32: :: QUANTAL1:32 for Q being Girard-Quantale for a being Element of Q holds ( a [*] (Top Q) = a & (Top Q) [*] a = a ) proof let Q be Girard-Quantale; ::_thesis: for a being Element of Q holds ( a [*] (Top Q) = a & (Top Q) [*] a = a ) let a be Element of Q; ::_thesis: ( a [*] (Top Q) = a & (Top Q) [*] a = a ) the absurd of Q is dualizing by Def20; then A1: Top Q = the_unity_wrt H4(Q) by Th19; H4(Q) is having_a_unity by MONOID_0:def_10; hence ( a [*] (Top Q) = a & (Top Q) [*] a = a ) by A1, SETWISEO:15; ::_thesis: verum end; theorem :: QUANTAL1:33 for Q being Girard-Quantale for a being Element of Q holds ( a delta (Bottom Q) = a & (Bottom Q) delta a = a ) proof let Q be Girard-Quantale; ::_thesis: for a being Element of Q holds ( a delta (Bottom Q) = a & (Bottom Q) delta a = a ) let a be Element of Q; ::_thesis: ( a delta (Bottom Q) = a & (Bottom Q) delta a = a ) ( (Bottom a) [*] (Top Q) = Bottom a & (Top Q) [*] (Bottom a) = Bottom a ) by Th32; hence ( a delta (Bottom Q) = a & (Bottom Q) delta a = a ) by Th22; ::_thesis: verum end; theorem :: QUANTAL1:34 for Q being Quantale for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds ex L being complete Lattice st ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) proof let Q be Quantale; ::_thesis: for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds ex L being complete Lattice st ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) let j be UnOp of Q; ::_thesis: ( j is monotone & j is idempotent & j is \/-distributive implies ex L being complete Lattice st ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) ) assume A1: ( j is monotone & j is idempotent & j is \/-distributive ) ; ::_thesis: ex L being complete Lattice st ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) reconsider D = rng j as non empty Subset of Q ; dom j = H1(Q) by FUNCT_2:def_1; then reconsider j9 = j as Function of H1(Q),D by RELSET_1:4; deffunc H5( Subset of D) -> Element of D = j9 . ("\/" (\$1,Q)); consider f being Function of (bool D),D such that A2: for X being Subset of D holds f . X = H5(X) from FUNCT_2:sch_4(); A3: dom f = bool D by FUNCT_2:def_1; A4: for X being Subset-Family of D holds f . (f .: X) = f . (union X) proof let X be Subset-Family of D; ::_thesis: f . (f .: X) = f . (union X) set A = { (j . a) where a is Element of Q : a in f .: X } ; set B = { (j . b) where b is Element of Q : b in union X } ; reconsider Y = f .: X, X9 = union X as Subset of Q by XBOOLE_1:1; now__::_thesis:_for_a_being_Element_of_Q_st_a_in__{__(j_._b)_where_b_is_Element_of_Q_:_b_in_union_X__}__holds_ ex_b_being_Element_of_the_carrier_of_Q_st_ (_a_[=_b_&_b_in__{__(j_._a)_where_a_is_Element_of_Q_:_a_in_f_.:_X__}__) let a be Element of Q; ::_thesis: ( a in { (j . b) where b is Element of Q : b in union X } implies ex b being Element of the carrier of Q st ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) ) assume a in { (j . b) where b is Element of Q : b in union X } ; ::_thesis: ex b being Element of the carrier of Q st ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) then consider b9 being Element of Q such that A5: a = j . b9 and A6: b9 in union X ; consider Y being set such that A7: b9 in Y and A8: Y in X by A6, TARSKI:def_4; reconsider Y = Y as Subset of D by A8; A9: b9 [= "\/" (Y,Q) by A7, LATTICE3:38; take b = j . ("\/" (Y,Q)); ::_thesis: ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) 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 { (j . a) where a is Element of Q : a in f .: X } ) by A1, A5, A10, A9, Def12; ::_thesis: verum end; then A11: "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) [= "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) by LATTICE3:47; { (j . a) where a is Element of Q : a in f .: X } is_less_than "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) proof let a be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not a in { (j . a) where a is Element of Q : a in f .: X } or a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) ) assume a in { (j . a) where a is Element of Q : a in f .: X } ; ::_thesis: a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) then consider a9 being Element of Q such that A12: a = j . a9 and A13: a9 in f .: X ; consider x being set 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 = x as Subset of D by A14; reconsider Y = x as Subset of Q by XBOOLE_1:1; A17: { (j . b) where b is Element of Q : b in Y } c= { (j . b) where b is Element of Q : b in union X } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (j . b) where b is Element of Q : b in Y } or z in { (j . b) where b is Element of Q : b in union X } ) assume z in { (j . b) where b is Element of Q : b in Y } ; ::_thesis: z in { (j . b) where b is Element of Q : b in union X } then consider b being 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 z in { (j . b) where b is Element of Q : b in union X } by A18; ::_thesis: verum end; a9 = j . ("\/" Y) by A2, A16; then a9 = "\/" ( { (j . b) where b is Element of Q : b in Y } ,Q) by A1, Th10; then a9 [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A17, LATTICE3:45; then a [= j . ("\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)) by A1, A12, Def12; then a [= j . (j . ("\/" X9)) by A1, Th10; then a [= j . ("\/" X9) by A1, Lm1; hence a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A1, Th10; ::_thesis: verum end; then A20: "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by LATTICE3:def_21; thus f . (f .: X) = j . ("\/" Y) by A2 .= "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) by A1, Th10 .= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A20, A11, LATTICES:8 .= j . ("\/" X9) by A1, Th10 .= f . (union X) by A2 ; ::_thesis: verum end; for a being Element of D holds f . {a} = a proof let a be Element of D; ::_thesis: f . {a} = a consider a9 being set 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 = 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 ; ::_thesis: verum end; then consider L being strict complete Lattice such that A23: H1(L) = D and A24: for X being Subset of L holds "\/" X = f . X by A4, LATTICE3:55; take L ; ::_thesis: ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) thus H1(L) = rng j by A23; ::_thesis: for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) let X be Subset of L; ::_thesis: "\/" X = j . ("\/" (X,Q)) thus "\/" X = f . X by A24 .= j . ("\/" (X,Q)) by A2, A23 ; ::_thesis: verum end;