let A be Element of LTLB_WFF ; :: thesis: [(<*> LTLB_WFF),<*A*>] ^ = TVERUM '&&' ('not' A)
( nega <*A*> = <*('not' A)*> & [(<*> LTLB_WFF),<*A*>] `1 = <*> LTLB_WFF ) by LTLAXIO2:14;
hence [(<*> LTLB_WFF),<*A*>] ^ = TVERUM '&&' ('not' A) by LTLAXIO2:10, LTLAXIO2:11; :: thesis: verum