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 ;
TARSKI:def 3 ( 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 ) }
;
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):]
;
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)
; verum