for A being Element of LTLB_WFF st TVERUM '&&' A is satisfiable holds
A is satisfiable