:: deftheorem defines '&&' LTLAXIO1:def 4 :
for p, q being Element of LTLB_WFF holds p '&&' q = 'not' (p => ('not' q));