theorem Th67: :: FILTER_0:67

for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is Equivalence_Relation of the carrier of L