for L being Lattice
for p being Element of L
for p9 being Element of (L .:) holds
( .: (p .:) = p & (.: p9) .: = p9 ) ;