theorem Th27: :: LTLAXIO1:27

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A => B & F |= A => ('X' A) holds
F |= A => ('G' B)