:: deftheorem defines |=0 LTLAXIO5:def 1 :
for M being LTLModel
for A being Element of LTLB_WFF holds
( M |=0 A iff (SAT M) . [0,A] = 1 );