theorem Th19: :: FILTER_0:19

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