theorem Th64: :: FILTER_0:64

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