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 { (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
A1: ( x = Bottom a & a in { (Bottom b) where b is Element of Q : b in X } ) ;
consider b being Element of Q such that
A2: ( a = Bottom b & b in X ) by A1;
thus x in X by A1, A2, Th22; :: thesis: verum

end;

then A3: "/\" 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:46;
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 ( 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 LATTICE3:38; :: thesis: verum

end;

then "/\" { (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:40;
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 A3, LATTICES:26;
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