theorem Th27: :: LTLAXIO3:27

[(<*> LTLB_WFF),(<*> LTLB_WFF)] ^ = TVERUM '&&' TVERUM