:: deftheorem defines Bottom QUANTAL1:def 21 :
for G being Girard-QuantaleStr holds Bottom G = the absurd of G;