for A being Element of LTLB_WFF st {} LTLB_WFF |=0 A holds
{} LTLB_WFF |=0 'X' A