:: deftheorem defines Top QUANTAL1:def 22 :
for G being non empty Girard-QuantaleStr holds Top G = (Bottom G) -r> (Bottom G);