for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A is LTL_TAUT_OF_PL holds
F |= A