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