theorem Th57: :: LTLAXIO1:57

for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F \/ {p} |- q holds
F |- ('G' p) => q