A3: w |= * (CastNode (N,v)) by A2, Def16;
( N in LTLNodes v & not CastNode (N,v) is elementary ) by A1, Def16, Def30;
hence ex b₁ being Nat st
( ( for i being Nat st i < b₁ holds
( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b₁) . N),v) is elementary & ( for i being Nat st i <= b₁ holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) ) by A3, Th51, Th62; :: thesis: verum