theorem :: FILTER_0:68

for L being Lattice
for F being Filter of L st L is I_Lattice holds
field (equivalence_wrt F) = the carrier of L