set X = { y where y is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;
{ y where y is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } c= [:(LTLStates v),AtomicFamily ,(LTLStates v):]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } or a in [:(LTLStates v),AtomicFamily ,(LTLStates v):] )
assume a in { y where y is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ; :: thesis: a in [:(LTLStates v),AtomicFamily ,(LTLStates v):]
then consider y being Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] such that
B1: ( a = y & ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) ) ;
thus a in [:(LTLStates v),AtomicFamily ,(LTLStates v):] by B1; :: thesis: verum

end;

then { y where y is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } c= [:[:(LTLStates v),AtomicFamily :],(LTLStates v):] by ZFMISC_1:def 3;
then reconsider X = { y where y is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } as Relation of [:(LTLStates v),AtomicFamily :],(LTLStates v) ;
X is Relation of [:(LTLStates v),AtomicFamily :],(LTLStates v) ;
hence { y where y is Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] : ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } is Relation of [:(LTLStates v),AtomicFamily :],(LTLStates v) ; :: thesis: verum