set X = { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } ;
{ x where x is Element of bool (LTLStates v) : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } c= bool (LTLStates v)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } or y in bool (LTLStates v) )
assume y in { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } ; :: thesis: y in bool (LTLStates v)
then ex x being Element of bool (LTLStates v) st
( y = x & ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) ) ;
hence y in bool (LTLStates v) ; :: thesis: verum

end;

hence { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } is Subset of (bool (LTLStates v)) ; :: thesis: verum