theorem :: FILTER_2:30

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