:: deftheorem Def9 defines LTL_WFF MODELC_2:def 9 :
for b₁ being non empty set holds
( b₁ = LTL_WFF iff ( ( for a being set st a in b₁ holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in b₁ ) & ( for p being FinSequence of NAT st p in b₁ holds
'not' p in b₁ ) & ( for p, q being FinSequence of NAT st p in b₁ & q in b₁ holds
p '&' q in b₁ ) & ( for p, q being FinSequence of NAT st p in b₁ & q in b₁ holds
p 'or' q in b₁ ) & ( for p being FinSequence of NAT st p in b₁ holds
'X' p in b₁ ) & ( for p, q being FinSequence of NAT st p in b₁ & q in b₁ holds
p 'U' q in b₁ ) & ( for p, q being FinSequence of NAT st p in b₁ & q in b₁ holds
p 'R' q in b₁ ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
b₁ c= D ) ) );