theorem Th5: :: LTLAXIO3:5

for A being Element of LTLB_WFF st not A is conditional holds
tau1 . A = {A}