:: deftheorem defines Bottom QUANTAL1:def 23 :
for G being non empty Girard-QuantaleStr
for a being Element of G holds Bottom a = a -r> (Bottom G);