theorem Th37: :: LTLAXIO1:37

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) holds
F |= A