theorem Th28: :: FILTER_2:28

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