set X = { y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over 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 over 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 object ; :: 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 over 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 over 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 ex y being Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] st
( a = y & ex s, s1 being strict elementary LTLnode over v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) ) ;
hence a in [:(LTLStates v),AtomicFamily,(LTLStates v):] ; :: thesis: verum

end;

then reconsider X = { y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over 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) by ZFMISC_1:def 3;
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 over 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