theorem th263pb: :: LTLAXIO5:20

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