theorem Orthogonalization.MvN.orthAtN_of_net {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {z : H →L[ℂ] H} (hz : Blocks.IsCentralProj M z) {κ : Type u} [Preorder κ] [IsDirected κ fun (x1 x2 : κ) => x1 ≤ x2] [Nonempty κ] (p : κ → H →L[ℂ] H) (hp : ∀ (α : κ), IsStarProjection (p α) ∧ p α ∈ M ∧ p α * z = p α) (hlim : CommutingRepetition.VN.TendstoStrongBdd Filter.atTop p z) (ι : Type u_1) [Fintype ι] (h : ∀ (α : κ), OrthAtN M (p α) ι) : OrthAtN M z ι

The semifinite reduction (step S).