:: deftheorem defines 'or' MODELC_1:def 20 :
for F, G being CTL-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G));