theorem :: FILTER_0:55

for L being Lattice
for F being Filter of L st L is I_Lattice holds
latt F is implicative