let x be set ; :: thesis: for v being LTL-formula holds
( x is Element of LTLStates v iff ex s being strict elementary LTLnode over v st s = x )
let v be LTL-formula; :: thesis: ( x is Element of LTLStates v iff ex s being strict elementary LTLnode over v st s = x )
( x is Element of LTLStates v implies ex s being strict elementary LTLnode over v st s = x )
proof
assume x is Element of LTLStates v ; :: thesis: ex s being strict elementary LTLnode over v st s = x
then x in LTLStates v ;
then consider y being Element of LTLNodes v such that
A1: y = x and
A2: y is strict elementary LTLnode over v ;
reconsider y = y as strict elementary LTLnode over v by A2;
take y ; :: thesis: y = x
thus y = x by A1; :: thesis: verum
end;
hence ( x is Element of LTLStates v iff ex s being strict elementary LTLnode over v st s = x ) by Th44; :: thesis: verum