theorem th267: :: LTLAXIO5:44

for A being Element of LTLB_WFF st {} LTLB_WFF |- A holds
{} LTLB_WFF |-0 A