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, z be object ; :: according to RELAT_1:def 3 :: 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 A1: ( y in field (equivalence_wrt F) & z in field (equivalence_wrt F) ) by RELAT_1:15;
field (equivalence_wrt F) c= the carrier of L by Def11;
hence [y,z] in [: the carrier of L, the carrier of L:] by A1, ZFMISC_1:87; :: thesis: verum

end;

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