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