for L being Lattice
for p being Element of L st ex r being Element of L st p "/\" r <> p holds
<.p.) <> the carrier of L