Re: push cannot be redirected in 4.1.5

[Viktor Szépe]

I am surprised of these different values:

echo "MAIN $BASHPID" ; echo "first $BASHPID" >&2 | echo "subshell $BASHPID"
MAIN 30551
subshell 8514
first 8513

Why neither side of the pipe has pid 30551?
Why are TWO new subshells needed?