for L being non empty LattStr holds
( the carrier of L = the carrier of (L .:) & the L_join of L = the L_meet of (L .:) & the L_meet of L = the L_join of (L .:) ) ;