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 be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in the carrier of L or not b₁ in the carrier of L or not b₂ in the carrier of L or not [x,b₁] in equivalence_wrt F or not [b₁,b₂] in equivalence_wrt F or [x,b₂] in equivalence_wrt F )
let y, z be set ; :: 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 Def12;
then p <=> r in F by A1, Th78;
hence [x,z] in equivalence_wrt F by Def12; :: thesis: verum