for A being Element of LTLB_WFF
for M being LTLModel holds
( M |= A iff M |= {A} )