theorem Th56: :: LTLAXIO1:56

for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- q holds
F \/ {p} |- q