theorem Th1: :: FILTER_1:1
for L being Lattice
for F1, F2 being Filter of L holds F1 /\ F2 is Filter of L