len (<*> LTLB_WFF) = 0 ;
then len (nega (<*> LTLB_WFF)) = 0 by LTLAXIO2:def 4;
then nega (<*> LTLB_WFF) = 0 ;
hence [(<*> LTLB_WFF),(<*> LTLB_WFF)] ^ = TVERUM '&&' TVERUM by LTLAXIO2:10; :: thesis: verum