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