:: deftheorem defines 'or' MODELC_1:def 38 :
for V being CTLModel
for f, g being Assign of V holds f 'or' g = 'not' (('not' f) '&' ('not' g));