theorem Th22: :: FILTER_2:22
for L being Lattice
for p, q being Element of L
for I being Ideal of L st p in I holds
( p "/\" q in I & q "/\" p in I )