theorem :: YELLOW13:10

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