:: deftheorem defines REFL0_rule LTLAXIO5:def 6 :
for p, q being Element of LTLB_WFF holds
( p REFL0_rule q iff p = 'G' q );