theorem Th4: :: LTLAXIO5:31

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