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
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 A1: 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 A1, LATTICE3:38; :: thesis: verum

end;

then A2: "/\" { (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;
{ (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
A3: ( x = Bottom a & a in { (Bottom b) where b is Element of Q : b in X } ) ;
ex b being Element of Q st
( a = Bottom b & b in X ) by A3;
hence x in X by A3, Th22; :: thesis: verum

end;

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 LATTICE3:46;
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 A2, 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