LTLStates v c= LTLNodes v

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in LTLStates v or a in LTLNodes v )
assume a in LTLStates v ; :: thesis: a in LTLNodes v
then ex x being Element of LTLNodes v st
( a = x & x is strict elementary LTLnode over v ) ;
hence a in LTLNodes v ; :: thesis: verum

end;

hence LTLStates v is finite ; :: thesis: verum