Description: Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)