theorem Th25: :: QUANTAL1:25

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)