theorem :: LTLAXIO1:30

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F \/ {A} |= B iff F |= ('G' A) => B )