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 ("\/" 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
A1: ( b = Bottom a & a in X ) ;
a [= "\/" X,Q by A1, LATTICE3:38;
hence Bottom ("\/" X,Q) [= b by A1, Th13; :: thesis: verum

end;

then A2: Bottom ("\/" X,Q) [= "/\" { (Bottom a) where a is Element of Q : a in X } ,Q by LATTICE3:40;
{ (("/\" { (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
A3: ( 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 A3;
then ( "/\" { (Bottom a) where a is Element of Q : a in X } ,Q [= Bottom b & Bottom b = b -r> (Bottom Q) ) by LATTICE3:38;
hence c [= Bottom Q by A3, 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 & Bottom ("\/" X,Q) = ("\/" X,Q) -r> (Bottom Q) ) by Def5;
then "/\" { (Bottom a) where a is Element of Q : a in X } ,Q [= Bottom ("\/" X,Q) by Th12;
hence Bottom ("\/" X,Q) = "/\" { (Bottom a) where a is Element of Q : a in X } ,Q by A2, LATTICES:26; :: thesis: verum