Description: Closure of a projection in its subspace. If we consider this together
with axpjpj to be axioms, the need for the ax-hcompl can often be
avoided for the kinds of theorems we are interested in here. An
interesting project is to see how far we can go by using them in place
of it. In particular, we can prove the orthomodular law pjomli .)
(Contributed by NM, 23-Oct-1999)(Revised by Mario Carneiro, 15-May-2014)(New usage is discouraged.)
|- ( ( H e. CH /\ A e. ~H ) -> ( ( ( projh ` H ) ` A ) = ( ( projh ` H ) ` A ) <-> ( ( ( projh ` H ) ` A ) e. H /\ E. x e. ( _|_ ` H ) A = ( ( ( projh ` H ) ` A ) +h x ) ) ) )