:: deftheorem defines MP0_rule LTLAXIO5:def 8 :
for p, q, r being Element of LTLB_WFF holds
( p,q MP0_rule r iff ex A, B being Element of LTLB_WFF st
( p = 'G' A & q = 'G' (A => B) & r = 'G' B ) );