theorem Th7: :: LTLAXIO4:7

for A being Element of LTLB_WFF holds [(<*> LTLB_WFF),<*A*>] ^ = TVERUM '&&' ('not' A)