puzzeling with Smullyan's "forever Undecided"

I am trying to find the solution to the exercise on page 111 of
"Forever undecided" by Raymond Smullyan

the question is to prove

(B(p < --> ~Bp} & B(-B_|_)) -> B_|_
for a type 4 reasoner

For people who don't have the book (i like it very much) a type 4
reasoner has the following axioms
Outside the normal rules of natural deductione

1a (Ax)[x -> Bx]
All tautologies are Believed (but what B means is immaterial)
or maybe this should be formalized as
(Ax)[((x ->x) -> x) -> Bx]

1b (Ax)(Ay) [(Bx & B(x->y)) -> By]
Modus ponens in B

2 (Ax)(Ay) [B{(Bx & B{x->y)} -> By}]
Belief in 1b

3 (Ax) [Bx -> BBx]

4 (Ax) [B{Bx -> BBx}]

At least this is how I formalise the conditions of type 4 reasoners.
(see page 90 for Smullyan's defining conditions)
(This is also open to discussion)

.