theorem Th43: :: LTLAXIO1:43

for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p & X |- p => q holds
X |- q