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