theorem Th8: :: FILTER_0:8

for L being Lattice
for S being non empty Subset of L holds
( S is Filter of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) )