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

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 }

hence Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by A2, LATTICES:8; :: thesis: verum

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

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

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

then
Bottom ("\/" (X,Q)) [= "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
by LATTICE3:39;
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;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

hence Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by A2, LATTICES:8; :: thesis: verum