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 object ; :: 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