set f = choice_succ_func w,v,U;
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