for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |=0 B ) holds
{} LTLB_WFF |=0 A