:: deftheorem defines satisfiable LTLAXIO4:def 2 :
for A being Element of LTLB_WFF holds
( A is satisfiable iff ex M being LTLModel ex n being Element of NAT st (SAT M) . [n,A] = 1 );