theorem Th4: :: LTLAXIO4:4

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