theorem Th10: :: LTLAXIO2:10

(con (<*> LTLB_WFF)) /. (len (con (<*> LTLB_WFF))) = TVERUM