theorem :: QUANTAL1:23

for Q being Girard-Quantale
for a, b being Element of Q st a [= b holds
Bottom b [= Bottom a by Th13;