set f = choice_succ_func w,v,U;
set XN = 'X' N;
set n = chosen_succ_end_num w,v,U,('X' N);
set nextnode = CastNode (((choice_succ_func w,v,U) |** (chosen_succ_end_num w,v,U,('X' N))) . ('X' N)),v;

now

thus ( ( not 'X' N is elementary implies CastNode (((choice_succ_func w,v,U) |** (chosen_succ_end_num w,v,U,('X' N))) . ('X' N)),v is strict elementary LTLnode of v ) & ( 'X' N is elementary implies FinalNode v is strict elementary LTLnode of v ) & ( for b₁ being strict elementary LTLnode of v holds verum ) ) by A1, Def48; :: thesis: verum

end;

hence ( ( not 'X' N is elementary implies CastNode (((choice_succ_func w,v,U) |** (chosen_succ_end_num w,v,U,('X' N))) . ('X' N)),v is strict elementary LTLnode of v ) & ( 'X' N is elementary implies FinalNode v is strict elementary LTLnode of v ) & ( for b₁ being strict elementary LTLnode of v holds verum ) ) ; :: thesis: verum