theorem Th23: :: LTLAXIO1:23

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