theorem Th24: :: QUANTAL1:24
for Q being Girard-Quantale
for X being set holds Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)