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 )
reconsider R = equivalence_wrt F as Relation of the carrier of L by Th63;
A1: R is_symmetric_in the carrier of L by Th65;
assume A2: L is I_Lattice ; :: thesis: equivalence_wrt F is Equivalence_Relation of the carrier of L
then R is_reflexive_in the carrier of L by Th64;
then A3: ( field R = the carrier of L & dom R = the carrier of L ) by ORDERS_1:13;
R is_transitive_in the carrier of L by A2, Th66;
hence equivalence_wrt F is Equivalence_Relation of the carrier of L by A3, A1, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum