theorem Th16: :: FILTER_0:16

for L being Lattice
for p, q being Element of L holds
( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) )