:: QUANTAL1 semantic presentation

scheme :: QUANTAL1:sch 1
s1{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> set , F₄( set ) -> Element of F₂(), P₁[ set ] } :

{ F₃(b₁) where B is Element of F₂() : b₁ in { F₄(b₂) where B is Element of F₁() : P₁[b₂] } } = { F₃(F₄(b₁)) where B is Element of F₁() : P₁[b₁] }

proof end;

scheme :: QUANTAL1:sch 2
s2{ F₁() -> non empty set , F₂( set ) -> set , P₁[ set ] } :

{ F₂(b₁) where B is Element of F₁() : P₁[b₁] } = {}

provided

E1: for b₁ being Element of F₁() holds P₁[b₁]

proof end;

deffunc H₁( non empty LattStr ) -> set = the carrier of a₁;

deffunc H₂( LattStr ) -> M5([:the carrier of a₁,the carrier of a₁:],the carrier of a₁) = the L_join of a₁;

deffunc H₃( LattStr ) -> M5([:the carrier of a₁,the carrier of a₁:],the carrier of a₁) = the L_meet of a₁;

deffunc H₄( HGrStr ) -> M5([:the carrier of a₁,the carrier of a₁:],the carrier of a₁) = the mult of a₁;

theorem Th1: :: QUANTAL1:1

for b₁, b₂ being non empty LattStr st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₃ = b₅ & b₄ = b₆ holds
( b₃ "\/" b₄ = b₅ "\/" b₆ & b₃ "/\" b₄ = b₅ "/\" b₆ & ( b₃ [= b₄ implies b₅ [= b₆ ) & ( b₅ [= b₆ implies b₃ [= b₄ ) )

proof end;

theorem Th2: :: QUANTAL1:2

for b₁, b₂ being non empty LattStr st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being set st b₃ = b₄ holds
( ( b₃ is_less_than b₅ implies b₄ is_less_than b₅ ) & ( b₄ is_less_than b₅ implies b₃ is_less_than b₅ ) & ( b₃ is_great_than b₅ implies b₄ is_great_than b₅ ) & ( b₄ is_great_than b₅ implies b₃ is_great_than b₅ ) )

proof end;

definition

let c₁ be 1-sorted ;
mode UnOp of a₁ is Function of a₁,a₁;

end;

definition

let c₁ be non empty LattStr ;
let c₂ be Subset of c₁;
attr a₂ is directed means :: QUANTAL1:def 1
for b₁ being finite Subset of a₂ ex b₂ being Element of a₁ st
( "\/" b₁,a₁ [= b₂ & b₂ in a₂ );

end;

:: deftheorem Def1 defines directed QUANTAL1:def 1 :

theorem Th3: :: QUANTAL1:3

for b₁ being non empty LattStr
for b₂ being Subset of b₁ st b₂ is directed holds
not b₂ is empty

proof end;

definition

attr a₁ is strict;
struct QuantaleStr -> LattStr , HGrStr ;
aggr QuantaleStr(# carrier, L_join, L_meet, mult #) -> QuantaleStr ;

end;

registration

cluster non empty QuantaleStr ;
existence

proof end;

end;

definition

attr a₁ is strict;
struct QuasiNetStr -> QuantaleStr , multLoopStr ;
aggr QuasiNetStr(# carrier, L_join, L_meet, mult, unity #) -> QuasiNetStr ;

end;

registration

cluster non empty QuasiNetStr ;
existence

proof end;

end;

definition

let c₁ be non empty HGrStr ;
attr a₁ is with_left-zero means :: QUANTAL1:def 2
ex b₁ being Element of a₁ st
for b₂ being Element of a₁ holds b₁ * b₂ = b₁;
attr a₁ is with_right-zero means :: QUANTAL1:def 3
ex b₁ being Element of a₁ st
for b₂ being Element of a₁ holds b₂ * b₁ = b₁;

end;

:: deftheorem Def2 defines with_left-zero QUANTAL1:def 2 :

:: deftheorem Def3 defines with_right-zero QUANTAL1:def 3 :

definition

let c₁ be non empty HGrStr ;
attr a₁ is with_zero means :Def4: :: QUANTAL1:def 4
( a₁ is with_left-zero & a₁ is with_right-zero );

end;

:: deftheorem Def4 defines with_zero QUANTAL1:def 4 :

registration

cluster non empty with_zero -> non empty with_left-zero with_right-zero HGrStr ;
coherence by Def4;
cluster non empty with_left-zero with_right-zero -> non empty with_zero HGrStr ;
coherence by Def4;

end;

registration

cluster non empty with_left-zero with_right-zero with_zero HGrStr ;
existence

proof end;

end;

definition

let c₁ be non empty QuantaleStr ;
attr a₁ is right-distributive means :Def5: :: QUANTAL1:def 5
for b₁ being Element of a₁
for b₂ being set holds b₁ [*] ("\/" b₂,a₁) = "\/" { (b₁ [*] b₃) where B is Element of a₁ : b₃ in b₂ } ,a₁;
attr a₁ is left-distributive means :Def6: :: QUANTAL1:def 6
for b₁ being Element of a₁
for b₂ being set holds ("\/" b₂,a₁) [*] b₁ = "\/" { (b₃ [*] b₁) where B is Element of a₁ : b₃ in b₂ } ,a₁;
attr a₁ is times-additive means :: QUANTAL1:def 7
for b₁, b₂, b₃ being Element of a₁ holds
( (b₁ "\/" b₂) [*] b₃ = (b₁ [*] b₃) "\/" (b₂ [*] b₃) & b₃ [*] (b₁ "\/" b₂) = (b₃ [*] b₁) "\/" (b₃ [*] b₂) );
attr a₁ is times-continuous means :: QUANTAL1:def 8
for b₁, b₂ being Subset of a₁ st b₁ is directed & b₂ is directed holds
("\/" b₁) [*] ("\/" b₂) = "\/" { (b₃ [*] b₄) where B is Element of a₁, B is Element of a₁ : ( b₃ in b₁ & b₄ in b₂ ) } ,a₁;

end;

:: deftheorem Def5 defines right-distributive QUANTAL1:def 5 :

:: deftheorem Def6 defines left-distributive QUANTAL1:def 6 :

:: deftheorem Def7 defines times-additive QUANTAL1:def 7 :

:: deftheorem Def8 defines times-continuous QUANTAL1:def 8 :

theorem Th4: :: QUANTAL1:4

for b₁ being non empty QuantaleStr st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = BooleLatt {} holds
( b₁ is associative & b₁ is commutative & b₁ is unital & b₁ is with_zero & b₁ is complete & b₁ is right-distributive & b₁ is left-distributive & b₁ is Lattice-like )

proof end;

registration

let c₁ be non empty set ;
let c₂, c₃, c₄ be BinOp of c₁;
cluster QuantaleStr(# a₁,a₂,a₃,a₄ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty Lattice-like complete unital associative commutative with_left-zero with_right-zero with_zero right-distributive left-distributive QuantaleStr ;
existence

proof end;

end;

scheme :: QUANTAL1:sch 3
s3{ F₁() -> non empty Lattice-like complete QuantaleStr , F₂( set , set ) -> Element of F₁(), F₃() -> set , F₄() -> set } :

"\/" { ("\/" { F₂(b₁,b₂) where B is Element of F₁() : b₂ in F₄() } ,F₁()) where B is Element of F₁() : b₁ in F₃() } ,F₁() = "\/" { F₂(b₁,b₂) where B is Element of F₁(), B is Element of F₁() : ( b₁ in F₃() & b₂ in F₄() ) } ,F₁()

proof end;

theorem Th5: :: QUANTAL1:5

for b₁ being non empty Lattice-like complete right-distributive left-distributive QuantaleStr
for b₂, b₃ being set holds ("\/" b₂,b₁) [*] ("\/" b₃,b₁) = "\/" { (b₄ [*] b₅) where B is Element of b₁, B is Element of b₁ : ( b₄ in b₂ & b₅ in b₃ ) } ,b₁

proof end;

theorem Th6: :: QUANTAL1:6

for b₁ being non empty Lattice-like complete right-distributive left-distributive QuantaleStr
for b₂, b₃, b₄ being Element of b₁ holds
( (b₂ "\/" b₃) [*] b₄ = (b₂ [*] b₄) "\/" (b₃ [*] b₄) & b₄ [*] (b₂ "\/" b₃) = (b₄ [*] b₂) "\/" (b₄ [*] b₃) )

proof end;

registration

let c₁ be non empty set ;
let c₂, c₃, c₄ be BinOp of c₁;
let c₅ be Element of c₁;
cluster QuasiNetStr(# a₁,a₂,a₃,a₄,a₅ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty Lattice-like complete QuasiNetStr ;
existence

proof end;

end;

registration

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

proof end;

end;

registration

cluster non empty Lattice-like complete unital associative commutative with_left-zero with_right-zero with_zero right-distributive left-distributive times-additive times-continuous QuasiNetStr ;
existence

proof end;

end;

definition

mode Quantale is non empty Lattice-like complete associative right-distributive left-distributive QuantaleStr ;
mode QuasiNet is non empty Lattice-like complete unital associative with_left-zero times-additive times-continuous QuasiNetStr ;

end;

definition

mode BlikleNet is non empty with_zero QuasiNet;

end;

theorem Th7: :: QUANTAL1:7

for b₁ being non empty unital QuasiNetStr st b₁ is Quantale holds
b₁ is BlikleNet

proof end;

theorem Th8: :: QUANTAL1:8

for b₁ being Quantale
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ holds
( b₂ [*] b₄ [= b₃ [*] b₄ & b₄ [*] b₂ [= b₄ [*] b₃ )

proof end;

theorem Th9: :: QUANTAL1:9

for b₁ being Quantale
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ [= b₃ & b₄ [= b₅ holds
b₂ [*] b₄ [= b₃ [*] b₅

proof end;

definition

let c₁ be Function;
attr a₁ is idempotent means :: QUANTAL1:def 9
a₁ * a₁ = a₁;

end;

:: deftheorem Def9 defines idempotent QUANTAL1:def 9 :

Lemma11: for b₁ being non empty set
for b₂ being UnOp of b₁ st b₂ is idempotent holds
for b₃ being Element of b₁ holds b₂ . (b₂ . b₃) = b₂ . b₃

proof end;

definition

let c₁ be non empty LattStr ;
let c₂ be UnOp of c₁;
attr a₂ is inflationary means :: QUANTAL1:def 10
for b₁ being Element of a₁ holds b₁ [= a₂ . b₁;
attr a₂ is deflationary means :: QUANTAL1:def 11
for b₁ being Element of a₁ holds a₂ . b₁ [= b₁;
attr a₂ is monotone means :Def12: :: QUANTAL1:def 12
for b₁, b₂ being Element of a₁ st b₁ [= b₂ holds
a₂ . b₁ [= a₂ . b₂;
attr a₂ is \/-distributive means :: QUANTAL1:def 13
for b₁ being Subset of a₁ holds a₂ . ("\/" b₁) [= "\/" { (a₂ . b₂) where B is Element of a₁ : b₂ in b₁ } ,a₁;

end;

:: deftheorem Def10 defines inflationary QUANTAL1:def 10 :

:: deftheorem Def11 defines deflationary QUANTAL1:def 11 :

:: deftheorem Def12 defines monotone QUANTAL1:def 12 :

:: deftheorem Def13 defines \/-distributive QUANTAL1:def 13 :

registration

let c₁ be Lattice;
cluster inflationary deflationary monotone M4(the carrier of a₁,the carrier of a₁);
existence

proof end;

end;

theorem Th10: :: QUANTAL1:10

for b₁ being complete Lattice
for b₂ being UnOp of b₁ st b₂ is monotone holds
( b₂ is \/-distributive iff for b₃ being Subset of b₁ holds b₂ . ("\/" b₃) = "\/" { (b₂ . b₄) where B is Element of b₁ : b₄ in b₃ } ,b₁ )

proof end;

definition

let c₁ be non empty QuantaleStr ;
let c₂ be UnOp of c₁;
attr a₂ is times-monotone means :: QUANTAL1:def 14
for b₁, b₂ being Element of a₁ holds (a₂ . b₁) [*] (a₂ . b₂) [= a₂ . (b₁ [*] b₂);

end;

:: deftheorem Def14 defines times-monotone QUANTAL1:def 14 :

definition

let c₁ be non empty QuantaleStr ;
let c₂, c₃ be Element of c₁;
func c₂ -r> c₃ -> Element of a₁ equals :: QUANTAL1:def 15
"\/" { b₁ where B is Element of a₁ : b₁ [*] a₂ [= a₃ } ,a₁;
correctness ;
func c₂ -l> c₃ -> Element of a₁ equals :: QUANTAL1:def 16
"\/" { b₁ where B is Element of a₁ : a₂ [*] b₁ [= a₃ } ,a₁;
correctness ;

end;

:: deftheorem Def15 defines -r> QUANTAL1:def 15 :

:: deftheorem Def16 defines -l> QUANTAL1:def 16 :

theorem Th11: :: QUANTAL1:11

for b₁ being Quantale
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ [*] b₃ [= b₄ iff b₃ [= b₂ -l> b₄ )

proof end;

theorem Th12: :: QUANTAL1:12

for b₁ being Quantale
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ [*] b₃ [= b₄ iff b₂ [= b₃ -r> b₄ )

proof end;

theorem Th13: :: QUANTAL1:13

for b₁ being Quantale
for b₂, b₃, b₄ being Element of b₁ st b₃ [= b₄ holds
( b₄ -r> b₂ [= b₃ -r> b₂ & b₄ -l> b₂ [= b₃ -l> b₂ )

proof end;

theorem Th14: :: QUANTAL1:14

for b₁ being Quantale
for b₂ being Element of b₁
for b₃ being UnOp of b₁ st ( for b₄ being Element of b₁ holds b₃ . b₄ = (b₄ -r> b₂) -r> b₂ ) holds
b₃ is monotone

proof end;

definition

let c₁ be non empty QuantaleStr ;
let c₂ be Element of c₁;
attr a₂ is dualizing means :Def17: :: QUANTAL1:def 17
for b₁ being Element of a₁ holds
( (b₁ -r> a₂) -l> a₂ = b₁ & (b₁ -l> a₂) -r> a₂ = b₁ );
attr a₂ is cyclic means :Def18: :: QUANTAL1:def 18
for b₁ being Element of a₁ holds b₁ -r> a₂ = b₁ -l> a₂;

end;

:: deftheorem Def17 defines dualizing QUANTAL1:def 17 :

:: deftheorem Def18 defines cyclic QUANTAL1:def 18 :

theorem Th15: :: QUANTAL1:15

for b₁ being Quantale
for b₂ being Element of b₁ holds
( b₂ is cyclic iff for b₃, b₄ being Element of b₁ st b₃ [*] b₄ [= b₂ holds
b₄ [*] b₃ [= b₂ )

proof end;

theorem Th16: :: QUANTAL1:16

for b₁ being Quantale
for b₂, b₃ being Element of b₁ st b₂ is cyclic holds
( b₃ [= (b₃ -r> b₂) -r> b₂ & b₃ [= (b₃ -l> b₂) -l> b₂ )

proof end;

theorem Th17: :: QUANTAL1:17

for b₁ being Quantale
for b₂, b₃ being Element of b₁ st b₂ is cyclic holds
( b₃ -r> b₂ = ((b₃ -r> b₂) -r> b₂) -r> b₂ & b₃ -l> b₂ = ((b₃ -l> b₂) -l> b₂) -l> b₂ )

proof end;

theorem Th18: :: QUANTAL1:18

for b₁ being Quantale
for b₂, b₃, b₄ being Element of b₁ st b₂ is cyclic holds
((b₃ -r> b₂) -r> b₂) [*] ((b₄ -r> b₂) -r> b₂) [= ((b₃ [*] b₄) -r> b₂) -r> b₂

proof end;

theorem Th19: :: QUANTAL1:19

for b₁ being Quantale
for b₂ being Element of b₁ st b₂ is dualizing holds
( b₁ is unital & the_unity_wrt the mult of b₁ = b₂ -r> b₂ & the_unity_wrt the mult of b₁ = b₂ -l> b₂ )

proof end;

theorem Th20: :: QUANTAL1:20

for b₁ being Quantale
for b₂, b₃, b₄ being Element of b₁ st b₂ is dualizing holds
( b₃ -r> b₄ = (b₃ [*] (b₄ -l> b₂)) -r> b₂ & b₃ -l> b₄ = ((b₄ -r> b₂) [*] b₃) -l> b₂ )

proof end;

definition

attr a₁ is strict;
struct Girard-QuantaleStr -> QuasiNetStr ;
aggr Girard-QuantaleStr(# carrier, L_join, L_meet, mult, unity, absurd #) -> Girard-QuantaleStr ;
sel absurd c₁ -> Element of the carrier of a₁;

end;

registration

cluster non empty Girard-QuantaleStr ;
existence

proof end;

end;

definition

let c₁ be non empty Girard-QuantaleStr ;
attr a₁ is cyclic means :Def19: :: QUANTAL1:def 19
the absurd of a₁ is cyclic;
attr a₁ is dualized means :Def20: :: QUANTAL1:def 20
the absurd of a₁ is dualizing;

end;

:: deftheorem Def19 defines cyclic QUANTAL1:def 19 :

:: deftheorem Def20 defines dualized QUANTAL1:def 20 :

theorem Th21: :: QUANTAL1:21

for b₁ being non empty Girard-QuantaleStr st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = BooleLatt {} holds
( b₁ is cyclic & b₁ is dualized )

proof end;

registration

let c₁ be non empty set ;
let c₂, c₃, c₄ be BinOp of c₁;
let c₅, c₆ be Element of c₁;
cluster Girard-QuantaleStr(# a₁,a₂,a₃,a₄,a₅,a₆ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty Lattice-like complete unital associative commutative right-distributive left-distributive times-additive times-continuous strict cyclic dualized Girard-QuantaleStr ;
existence

proof end;

end;

definition

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

end;

definition

let c₁ be Girard-QuantaleStr ;
func Bottom c₁ -> Element of a₁ equals :: QUANTAL1:def 21
the absurd of a₁;
correctness ;

end;

:: deftheorem Def21 defines Bottom QUANTAL1:def 21 :

definition

let c₁ be non empty Girard-QuantaleStr ;
func Top c₁ -> Element of a₁ equals :: QUANTAL1:def 22
(Bottom a₁) -r> (Bottom a₁);
correctness ;
let c₂ be Element of c₁;
func Bottom c₂ -> Element of a₁ equals :: QUANTAL1:def 23
a₂ -r> (Bottom a₁);
correctness ;

end;

:: deftheorem Def22 defines Top QUANTAL1:def 22 :

:: deftheorem Def23 defines Bottom QUANTAL1:def 23 :

definition

let c₁ be non empty Girard-QuantaleStr ;
func Negation c₁ -> UnOp of a₁ means :: QUANTAL1:def 24
for b₁ being Element of a₁ holds a₂ . b₁ = Bottom b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines Negation QUANTAL1:def 24 :

definition

let c₁ be non empty Girard-QuantaleStr ;
let c₂ be UnOp of c₁;
func Bottom c₂ -> UnOp of a₁ equals :: QUANTAL1:def 25
(Negation a₁) * a₂;
correctness ;

end;

:: deftheorem Def25 defines Bottom QUANTAL1:def 25 :

definition

let c₁ be non empty Girard-QuantaleStr ;
let c₂ be BinOp of c₁;
func Bottom c₂ -> BinOp of a₁ equals :: QUANTAL1:def 26
(Negation a₁) * a₂;
correctness ;

end;

:: deftheorem Def26 defines Bottom QUANTAL1:def 26 :

theorem Th22: :: QUANTAL1:22

for b₁ being Girard-Quantale
for b₂ being Element of b₁ holds Bottom (Bottom b₂) = b₂

proof end;

theorem Th23: :: QUANTAL1:23

for b₁ being Girard-Quantale
for b₂, b₃ being Element of b₁ st b₂ [= b₃ holds
Bottom b₃ [= Bottom b₂ by Th13;

theorem Th24: :: QUANTAL1:24

for b₁ being Girard-Quantale
for b₂ being set holds Bottom ("\/" b₂,b₁) = "/\" { (Bottom b₃) where B is Element of b₁ : b₃ in b₂ } ,b₁

proof end;

theorem Th25: :: QUANTAL1:25

for b₁ being Girard-Quantale
for b₂ being set holds Bottom ("/\" b₂,b₁) = "\/" { (Bottom b₃) where B is Element of b₁ : b₃ in b₂ } ,b₁

proof end;

theorem Th26: :: QUANTAL1:26

for b₁ being Girard-Quantale
for b₂, b₃ being Element of b₁ holds
( Bottom (b₂ "\/" b₃) = (Bottom b₂) "/\" (Bottom b₃) & Bottom (b₂ "/\" b₃) = (Bottom b₂) "\/" (Bottom b₃) )

proof end;

definition

let c₁ be Girard-Quantale;
let c₂, c₃ be Element of c₁;
func c₂ delta c₃ -> Element of a₁ equals :: QUANTAL1:def 27
Bottom ((Bottom a₂) [*] (Bottom a₃));
correctness ;

end;

:: deftheorem Def27 defines delta QUANTAL1:def 27 :

theorem Th27: :: QUANTAL1:27

for b₁ being Girard-Quantale
for b₂ being Element of b₁
for b₃ being set holds
( b₂ [*] ("\/" b₃,b₁) = "\/" { (b₂ [*] b₄) where B is Element of b₁ : b₄ in b₃ } ,b₁ & b₂ delta ("/\" b₃,b₁) = "/\" { (b₂ delta b₄) where B is Element of b₁ : b₄ in b₃ } ,b₁ )

proof end;

theorem Th28: :: QUANTAL1:28

for b₁ being Girard-Quantale
for b₂ being Element of b₁
for b₃ being set holds
( ("\/" b₃,b₁) [*] b₂ = "\/" { (b₄ [*] b₂) where B is Element of b₁ : b₄ in b₃ } ,b₁ & ("/\" b₃,b₁) delta b₂ = "/\" { (b₄ delta b₂) where B is Element of b₁ : b₄ in b₃ } ,b₁ )

proof end;

theorem Th29: :: QUANTAL1:29

for b₁ being Girard-Quantale
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ delta (b₃ "/\" b₄) = (b₂ delta b₃) "/\" (b₂ delta b₄) & (b₃ "/\" b₄) delta b₂ = (b₃ delta b₂) "/\" (b₄ delta b₂) )

proof end;

theorem Th30: :: QUANTAL1:30

for b₁ being Girard-Quantale
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ [= b₃ & b₄ [= b₅ holds
b₂ delta b₄ [= b₃ delta b₅

proof end;

theorem Th31: :: QUANTAL1:31

for b₁ being Girard-Quantale
for b₂, b₃, b₄ being Element of b₁ holds (b₂ delta b₃) delta b₄ = b₂ delta (b₃ delta b₄)

proof end;

theorem Th32: :: QUANTAL1:32

for b₁ being Girard-Quantale
for b₂ being Element of b₁ holds
( b₂ [*] (Top b₁) = b₂ & (Top b₁) [*] b₂ = b₂ )

proof end;

theorem Th33: :: QUANTAL1:33

for b₁ being Girard-Quantale
for b₂ being Element of b₁ holds
( b₂ delta (Bottom b₁) = b₂ & (Bottom b₁) delta b₂ = b₂ )

proof end;

theorem Th34: :: QUANTAL1:34

for b₁ being Quantale
for b₂ being UnOp of b₁ st b₂ is monotone & b₂ is idempotent & b₂ is \/-distributive holds
ex b₃ being complete Lattice st
( the carrier of b₃ = rng b₂ & ( for b₄ being Subset of b₃ holds "\/" b₄ = b₂ . ("\/" b₄,b₁) ) )

proof end;