let n be Nat; :: thesis: for v being LTL-formula
for q being sequence of (LTLStates v) ex s being strict elementary LTLnode over v st s = CastNode ((q . n),v)
let v be LTL-formula; :: thesis: for q being sequence of (LTLStates v) ex s being strict elementary LTLnode over v st s = CastNode ((q . n),v)
let q be sequence of (LTLStates v); :: thesis: ex s being strict elementary LTLnode over v st s = CastNode ((q . n),v)
reconsider n = n as Element of NAT by ORDINAL1:def 12;
consider s being strict elementary LTLnode over v such that
A1: s = q . n by Th45;
CastNode ((q . n),v) = s by A1, Def16;
hence ex s being strict elementary LTLnode over v st s = CastNode ((q . n),v) ; :: thesis: verum