:: deftheorem Def12 defines |= LTLAXIO1:def 12 :
for M being LTLModel
for p being Element of LTLB_WFF holds
( M |= p iff for n being Element of NAT holds (SAT M) . [n,p] = 1 );