:: deftheorem Def19 defines cyclic QUANTAL1:def 19 :
for IT being non empty Girard-QuantaleStr holds
( IT is cyclic iff the absurd of IT is cyclic );