:: deftheorem defines without_implication LTLAXIO3:def 1 :
for X being Subset of LTLB_WFF holds
( X is without_implication iff for p being Element of LTLB_WFF st p in X holds
not p is conditional );