Editing Von Neumann bicommutant theorem (section)

===Proof of (iii)===
Fix {{math|''X'' ∈ '''M'''′′}}. We must show that {{math|''X'' ∈ cl<sub>''S''</sub>('''M''')}}, i.e. for each ''h'' ∈ ''H'' and any {{math|''ε'' > 0}}, there exists ''T'' in {{math|'''M'''}} with {{math|{{!!}}''Xh'' − ''Th''{{!!}} < ''ε''}}.

Fix ''h'' in {{mvar|H}}. The [[Cyclic subspace | cyclic subspace]] {{math|'''M'''''h'' {{=}} {''Mh'' : ''M'' ∈ '''M'''}}} is invariant under the action of any ''T'' in {{math|'''M'''}}. Its [[Closure (topology)|closure]] {{math|cl('''M'''''h'')}} in the norm of ''H'' is a closed linear subspace, with corresponding [[orthogonal projection]] {{mvar|P}} : ''H'' → {{math|cl('''M'''''h'')}} in ''L''(''H''). In fact, this ''P'' is in {{math|'''M'''′}}, as we now show.

:'''Lemma.''' {{math|''P'' ∈ '''M'''′}}.

:'''Proof.''' Fix {{math|''x'' ∈ ''H''}}. As {{math|''Px'' ∈ cl('''M'''''h'')}}, it is the limit of a sequence {{mvar|O<sub>n</sub>h}} with {{mvar|O<sub>n</sub>}} in {{math|'''M'''}}. For any {{math|''T'' ∈ '''M'''}}, {{mvar|TO<sub>n</sub>h}} is also in {{math|'''M'''''h''}}, and by the continuity of {{mvar|T}}, this sequence converges to {{mvar|TPx}}. So {{math|''TPx'' ∈ cl('''M'''''h'')}}, and hence ''PTPx'' = ''TPx''. Since ''x'' was arbitrary, we have ''PTP'' = ''TP'' for all {{mvar|T}} in {{math|'''M'''}}.  

:Since {{math|'''M'''}} is closed under the adjoint operation and ''P'' is [[self-adjoint operator|self-adjoint]], for any {{math|''x'', ''y'' ∈ ''H''}} we have

::<math>\langle x,TPy\rangle = \langle x,PTPy\rangle = \langle (PTP)^*x,y\rangle = \langle PT^*Px,y\rangle = \langle T^*Px,y\rangle = \langle Px,Ty\rangle = \langle x,PTy\rangle</math>

:So ''TP'' = ''PT'' for all {{math|''T'' ∈ '''M'''}}, meaning ''P'' lies in {{math|'''M'''′}}.

By definition of the [[bicommutant]], we must have ''XP'' = ''PX''. Since {{math|'''M'''}} is unital, {{math|''h'' ∈ '''M'''''h''}}, and so {{math| ''h'' {{=}} ''Ph''}}. Hence {{math|''Xh'' {{=}} ''XPh'' {{=}} ''PXh'' ∈ cl('''M'''''h'')}}. So for each {{math|''ε'' > 0}}, there exists ''T'' in {{math|'''M'''}} with {{math|{{!!}}''Xh'' − ''Th''{{!!}} < ''ε''}}, i.e. {{mvar|X}} is in the strong operator closure of {{math|'''M'''}}.