for N being finite LATTICE holds N, InclPoset (Ids N) are_isomorphic