set X = { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode x,v) or the_right_argument_of F in the LTLold of (CastNode x,v) ) } ;
{ x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode x,v) or the_right_argument_of F in the LTLold of (CastNode x,v) ) } c= LTLStates v

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode x,v) or the_right_argument_of F in the LTLold of (CastNode x,v) ) } or y in LTLStates v )
assume y in { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode x,v) or the_right_argument_of F in the LTLold of (CastNode x,v) ) } ; :: thesis: y in LTLStates v
then ex x being Element of LTLStates v st
( y = x & ( not F in the LTLold of (CastNode x,v) or the_right_argument_of F in the LTLold of (CastNode x,v) ) ) ;
hence y in LTLStates v ; :: thesis: verum

end;

hence { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode x,v) or the_right_argument_of F in the LTLold of (CastNode x,v) ) } is Element of bool (LTLStates v) ; :: thesis: verum