let L be Lattice; :: thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_transitive_in the carrier of L
let F be Filter of L; :: thesis: ( L is I_Lattice implies equivalence_wrt F is_transitive_in the carrier of L )
assume A1: L is I_Lattice ; :: thesis: equivalence_wrt F is_transitive_in the carrier of L
let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in the carrier of L or not y in the carrier of L or not z in the carrier of L or not [x,y] in equivalence_wrt F or not [y,z] in equivalence_wrt F or [x,z] in equivalence_wrt F )
assume ( x in the carrier of L & y in the carrier of L & z in the carrier of L ) ; :: thesis: ( not [x,y] in equivalence_wrt F or not [y,z] in equivalence_wrt F or [x,z] in equivalence_wrt F )
then reconsider p = x, q = y, r = z as Element of L ;
assume ( [x,y] in equivalence_wrt F & [y,z] in equivalence_wrt F ) ; :: thesis: [x,z] in equivalence_wrt F
then ( p <=> q in F & q <=> r in F ) by Def11;
then p <=> r in F by A1, Th62;
hence [x,z] in equivalence_wrt F by Def11; :: thesis: verum