let L be Lattice; :: thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is Equivalence_Relation of the carrier of L
let F be Filter of L; :: thesis: ( L is I_Lattice implies equivalence_wrt F is Equivalence_Relation of the carrier of L )
assume A1: L is I_Lattice ; :: thesis: equivalence_wrt F is Equivalence_Relation of the carrier of L
reconsider R = equivalence_wrt F as Relation of the carrier of L by Th80;
( R is total & R is symmetric & R is transitive )

proof

R is_reflexive_in the carrier of L by A1, Th81;
then A2: ( field R = the carrier of L & dom R = the carrier of L ) by ORDERS_1:98;
hence R is total by PARTFUN1:def 4; :: thesis: ( R is symmetric & R is transitive )
( R is_symmetric_in the carrier of L & R is_transitive_in the carrier of L ) by A1, Th82, Th83;
hence ( R is symmetric & R is transitive ) by A2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum

end;

hence equivalence_wrt F is Equivalence_Relation of the carrier of L ; :: thesis: verum