:: deftheorem defines MP_rule LTLAXIO1:def 20 :
for p, q, r being Element of LTLB_WFF holds
( p,q MP_rule r iff q = p => r );