theorem Th36: :: FILTER_0:36

for L being Lattice
for H, F being Filter of L holds
( F c= F "/\" H & H c= F "/\" H )