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