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