theorem Th15: :: FILTER_0:15

for L being Lattice
for p, q being Element of L holds
( q in <.p.) iff p [= q )