let L be Lattice; :: thesis: for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L
let F be Filter of L; :: thesis: equivalence_wrt F is Relation of the carrier of L
equivalence_wrt F c= [:the carrier of L,the carrier of L:]

proof

let y be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [y,b₁] in equivalence_wrt F or [y,b₁] in [:the carrier of L,the carrier of L:] )
let z be set ; :: thesis: ( not [y,z] in equivalence_wrt F or [y,z] in [:the carrier of L,the carrier of L:] )
assume [y,z] in equivalence_wrt F ; :: thesis: [y,z] in [:the carrier of L,the carrier of L:]
then ( y in field (equivalence_wrt F) & z in field (equivalence_wrt F) & field (equivalence_wrt F) c= the carrier of L ) by Def12, RELAT_1:30;
hence [y,z] in [:the carrier of L,the carrier of L:] by ZFMISC_1:106; :: thesis: verum

end;

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