let L be Lattice; for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L
let F be Filter of L; 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 ;
RELAT_1:def 3 ( 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
;
[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;
verum
end;
hence
equivalence_wrt F is Relation of the carrier of L
; verum