:: 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;