:: deftheorem defines Release MODELC_2:def 17 :
for H being LTL-formula holds
( H is Release iff ex F, G being LTL-formula st H = F 'R' G );