The double commutation theorem for selfdual Hilbert right W*-modules

Let E be a W*-algebra, H a selfdual Hilbert right E-module, L(H) the W*-algebra of adjointable operators on H, and F an involutive unital subalgebra of L(H). We prove that the double commutant of F is the W*-subalgebra of L(H) generated by F. The proofs work simultaneously for the real and for the complex case. If E is the field of real or complex numbers then H is a Hilbert space and this result becomes the well-known classical double commutation theorem.