theorem th261bq: :: LTLAXIO5:12

for F being Subset of LTLB_WFF
for M being LTLModel holds
( M |= F iff M |=0 'G' F )