theorem Th3: :: LTLAXIO4:3

for A being Element of LTLB_WFF holds
( {} LTLB_WFF |= A iff not 'not' A is satisfiable )