theorem :: LATTICE2:13

for L being non empty strict LattStr holds (L .:) .: = L ;