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:40;
hence Bottom ("\/" X,Q) = "/\" { (Bottom a) where a is Element of Q : a in X } ,Q by A2, LATTICES:26; :: thesis: verum